Apología de la programación en Haskell
En el artículo Eleven Reasons to use Haskell as a Mathematician se realiza una apología del uso de Haskell como lenguaje de programación en matemáticas.
Read More “Apología de la programación en Haskell”
Apología de la programación en Lisp
Recientemente se ha publicado el artículo Why We Love Lisp que es una apología de la programación en Lisp.
Algunas de las aspectos de Lisp en las que se basa la apología son:
Read More “Apología de la programación en Lisp”
Anuncio: Trace-based verification of imperative programs with I/O
Gregory Malecha, Greg Morrisett y Ryan Wisnesky han publicado el artículo Trace-based verification of imperative programs with I/O en el Journal of Symbolic Computation. Una versión del artículo puede leerse aquí.
El resumen del artículo es
In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants.
Los autores son miembros del Grupo de Lenguajes de Programación de la Universidad de Harvard.
Este artículo está relacionado con el proyecto SAFE (Semantically Aware Foundation Environment) comentado en una entrada anterior.
El problema de la igualdad de los bordes de los árboles binarios (sameFringe)
Dos árboles binarios tienen iguales los bordes si tienen exactamente
las mismas hojas leídas de izquierda a derecha, independientemente de
nodos interiores. Por ejemplo,
|
1 2 3 4 5 6 |
árbol1 árbol2 árbol3 árbol4 o o o o / \ / \ / \ / \ 1 o o 3 o 3 o 1 / \ / \ / \ / \ 2 3 1 2 1 4 2 3 |
Los bordes de los árboles 1 y 2 son iguales, aunque tiene distintas
estructuras internas. El árbol 3 no tiene el mismo borde que el 1 o
el 2, debido al nodo 4. El árbol 4 tampoco tiene el mismo borde que
el 1 debido al orden en que se leen las hojas.
El problema de la igualdad de los bordes de los árboles binarios
(samefringe, en inglés) consiste en decidir si dos árboles tienen los bordes iguales.
Read More “El problema de la igualdad de los bordes de los árboles binarios (sameFringe)”
Trabajo de Lógica Computacional en las Universidades de Pensilvania, Harvard y Northeastern
Se ha anunciado la oferta de plazas postdoctorales en la Universidad de Pensilvania, la Universidad de Harvard y la Universidad Northeastern.
El trabajo se desarrollará dentro del proyecto SAFE (Semantically Aware Foundation Environment).
SAFE es parte del proyecto CRASH (Clean-Slate Design of Resilient, Adaptive, Secure Hosts)
CRASH es un gran proyecto financiado por la DARPA (Defense Advanced Research Projects Agency) cuyo objetivo es el diseño de nuevos sistemas computacionales que sean muy resistentes a los ciberataques. Se desea diseñar los niveles de hardware, sistemas operativos y lenguajes de programación poniendo el énfasis en la simplicidad, seguridad y verificabilidad de todos los niveles.
Las áreas de trabajo son lenguajes de programación, verificación formal, sistemas operativos y diseño de hardware.