Para instrucciones sobre cómo correr F* ver: Ejecutar.md.
Para instrucciones sobre cómo usar la extensión, ver aquí.
| # | Fecha | Tema |
|---|---|---|
| 1 | 12/03 | Introducción a verificación, F*, tipos refinados. |
| 2 | 19/03 | Tipos dependientes, lógica formal, Curry-Howard. |
| 3 | 26/03 | Recursión, terminación, tipos inductivos (índices, parámetros, GADTS), positividad. |
| 02/04 | Feriado. | |
| 4 | 09/04 | Más tipos indexados, pruebas extrínsecas. |
| 5 | 16/04 | SMT solvers, Codificación a SMT, verificando BSTs. |
| 6 | 23/04 | Más BSTs, invariantes, refinando una ED. |
| 7 | 30/04 | Lógica de Hoare (verificada) para Imp. |
| 07/05 | Cancelada. | |
| 8 | 14/05 | Weakest preconditions, construyendo un verificador (verificado). |
| 9 | 21/05 | Efectos en F* y verificación, Mónadas de Dijkstra. |
| 10 | 28/05 | Pruebas calculacionales. Breve intro a tácticas y metaprogramación (más material) |
| 04/06 | Cancelada. | |
| 11 | 11/06 | Invitada: Gabriel Ebner sobre Lean4 y Mathlib |
| 12 | 18/06 | Consultas, cierre |
| -- | 25/06 | Consulta |
- Proof-Oriented Programming in F*, capítulos 1-4, 6-8, 29 (por ahora)
- Hoare - An axiomatic basis for computer programming (1969)
- Métodos formales en la práctica
- Bugs famosos
- Bug FDIV del Pentium
- Vuelo Arianne V88
- Heartbleed: filtración de datos en OpenSSL
- Maleabilidad en Bitcoin, y Hackeo a MtGox
- Spectre y Meltdown: bugs de hardware relacionados a ejecución especulativa
- Casa Blanca EE.UU. - Back to the Building Blocks: A Path Toward Secure and Measurable Software (2024)
- Verificación
- Lenguajes de Programación
- Wadler - Theorems for free! (1989): parametricidad y teoremas gratis
- Wadler - Propositions as types (2015): correspondencia Curry-Howard
- Augustsson - Cayenne - a language with dependent types (1998)
- McBride - Faking it: Simulating dependent types in Haskell (2002)
- Verificación de programas con efectos
- Verificando verificadores