RA2017: Demostración en Isabelle de la corrección de un compilador

En la segunda parte de 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