-
Demostración de teoremas
Programar un mini-Lean en el sistema de tipos de Julia
Guillermo Angeris arma un demostrador de teoremas que funciona en 61 líneas de Julia. Un kernel de confianza chiquito, seis axiomas, y el compilador hace el resto. Esta es la construcción.
-
Demostración de teoremas
Construyendo un pequeño demostrador de teoremas en Python
Un pequeño demostrador de teoremas es apenas un lenguaje de términos, un checker y un kernel chico de confianza. Construimos uno en Python puro para dejar la arquitectura a la vista.
-
Demostración de teoremas
Las proposiciones son tipos, las demostraciones son programas
La correspondencia de Curry-Howard dice que los tipos y las proposiciones lógicas son lo mismo. Entender por qué cambia cómo pensás tanto la programación como la matemática.