RA2013: Demostración en Isabelle de la corrección de un compilador
En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.
La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2013: Demostración en Isabelle de la corrección de un compilador”