Un Enfoque Computacional para el Diseño de Verificadores de Tipos

Este artículo presenta un enfoque computacional para el diseño de verificadores de tipos, derivándolos de especificaciones de comportamiento utilizando razonamiento ecuacional. Los autores simplifican los cálculos utilizando un enfoque algebraico basado en la fusión de plegado y lo mejoran aún más con un enfoque basado en restricciones para resolver y componer precondiciones de fusión. La metodología se ilustra con tres ejemplos de complejidad creciente: un lenguaje de expresión simple, uno con excepciones y una versión del cálculo lambda.