| 1 |
12/03 |
Introducción a verificación, F*, tipos refinados. |
[pdf] |
Clase1.fst
|
| 2 |
19/03 |
Tipos dependientes, lógica formal, Curry-Howard. |
[pdf] |
Clase2.fst
Clase2.DeMorgan.fst
|
| 3 |
26/03 |
Recursión, terminación, tipos inductivos (índices, parámetros, GADTS), positividad. |
[pdf] |
Clase3.GADT.fst
Clase3.Positividad.fst
Clase3.Recursion.fst
|
| |
02/04 |
Feriado. |
|
|
| 4 |
09/04 |
Más tipos indexados, pruebas extrínsecas. |
[pdf] |
| 5 |
16/04 |
SMT solvers, Codificación a SMT, verificando BSTs. |
[pdf] |
Clase5.BST.fst
Clase5.Fib.fst
Clase5.Listas.fst
Clase5.MiniLang.fst
|
| 6 |
23/04 |
Más BSTs, invariantes, refinando una ED. |
[pdf] |
Clase6.BST.fst
|
| 7 |
30/04 |
Lógica de Hoare (verificada) para Imp. |
[pdf] |
Clase7.Imp.fst
|
| |
07/05 |
Cancelada. |
|
|
| 8 |
14/05 |
Weakest preconditions, construyendo un verificador (verificado). |
[pdf] |
Clase8.WP.fst
|
| 9 |
21/05 |
Efectos en F* y verificación, Mónadas de Dijkstra. |
[pdf] |
Clase9.Eff.fst (ver repositorio para Makefile y archivos de Dune).
|
| 10 |
28/05 |
Pruebas calculacionales. Breve intro a tácticas y metaprogramación (más material). |
[pdf]
[metafstar]
|
Clase10.Calc.fst
Clase10.Tac.Automation.fst
Clase10.Tac.Constructive.fst
Clase10.Tac.Hybrid.fst
Clase10.Tac.Intro.fst
|
| |
04/06 |
Cancelada. |
|
|
| 11 |
11/06 |
Invitada: Gabriel Ebner sobre Lean4 y Mathlib.
| |
Repositorio |
| 12 |
18/06 |
Invitada: Jonathan Protzenko. |
[pdf]
|
Tuto.fst
Tuto.c
Tuto.h
|
| 13 |
25/06 |
Clases de tipo y abstracción, ejemplo de entrega de proyecto. |
[pdf]
|
Clase13.DEQ.fst
Container.fst
Clase13.Listas.fst
Clase13.Listas.fsti
Clase13.Cliente.fst
Container.Indexed.fst
Clase13.Cliente.Indexed.fst
|