DAO2012: Programación funcional en Isabelle
En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2011) se ha presentado Isabelle como un sistema de programación funcional que permite
- evaluar expresiones aritméticas y lógicas (con value),
- definir funciones no recursivas (con definition),
- definir funciones recursivas (con fun),
- enunciar propiedades (con lemma) y
- demostrar propiedades por simplificación (con simp).
La teoría correspondiente a la clase es T2_Programacion_funcional_en_Isabelle.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Programación funcional en Isabelle”