Matemáticas, lógica e informática
Florent Schaffhauser, Universidad de Heidelberg
Información general
- Cursillo de 8 horas, en celebración de los 60 años de la carrera de matemáticas de la Universidad de Los Andes (Bogotá) y en honor a Xavier Caicedo.
- Tema: una introducción a las matemáticas formales, dirigido hacia personas interesadas en la interacción entre matemáticas, lógica e informática.
- Conferencista: Florent Schaffhauser.
- Horario: 10 AM -12 PM, el lunes 2, martes 3, jueves 5 y viernes 6 de diciembre 2024.
Objetivos
En este taller, exploramos el mundo de los asistentes de prueba y aprendemos a hacer demostraciones por computador usando Lean, un lenguaje de programación funcional creado por Leonardo de Moura en 2013. El objetivo es que los participantes se familiaricen con los métodos formales y desarrollen habilidades de programación nuevas.
Organización del curso
El curso consta de cuatro sesiones de dos horas cada una. En cada sesión, se combinará la parte teórica con unos ejercicios prácticos, realizados por computador.
Se les recomienda a los participantes que trabajen en grupos de dos personas. En cada sesión, se proporcionarán archivos para practicar. No se requiere instalación previa de Lean y un tablet ya es suficiente para tener acceso al material del taller.
| Clase | Tema | Archivos para practicar |
|---|---|---|
| 1 | Sintaxis básica | |
| 2 | Tácticas | |
| 3 | Tipos dependientes | |
| 4 | Estructuras algebraicas |
Diseño y construcción
Página producida con Quarto Markdown y VS Code. Diapositivas producidas usando Marp, también desde VS Code. Esta página web se publica a través de GitHub Pages. Los códigos QR fueron creados con Python, usando el package qrcode.