RA2010: Demostración con Isabelle de la corrección de un compilador
En la clase de hoy del curso de Razonamiento automático se ha estudiado como caso de estudio, la formalización de un compilador de expresiones aritméticas y la demostración de su corrección en Isabelle. El contenido de la clase se encuentra en el tema 6 y el código correspondiente se encuentra en Cap_6.thy .