| # | Fecha | Tema | Diapositivas | Material |
|---|---|---|---|---|
| 1 | 28/08 | Introducción a verificación, F*, tipos refinados. | [pdf] | Clase01.fst |
| 2 | 04/09 | Tipos dependientes, lógica formal, Curry-Howard. | [pdf] | Clase02.fst |
| 3 | 11/09 | Recursión, terminación, tipos inductivos (índices, parámetros, GADTS), positividad. | [pdf] | Clase03.GADT.fst Clase03.Positividad.fst Clase03.Recursion.fst Clase03.Vec.fst |
| 4 | 18/09 | Más tipos indexados, pruebas extrínsecas. | [pdf] | Clase04.BST.fst Clase04.Fib.fst Clase04.Listas.fst Clase04.MiniLang.fst |
| 5 | 25/09 | Más BSTs, invariantes, refinando una ED. Algo de resolución SMT. | [pdf] | Clase05.BST.fst sudoku.smt2 |
| 6 | 02/10 | Lógica de Hoare (verificada) para Imp. | [pdf] | Clase06.Imp.fst |
| 7 | 09/10 | Weakest preconditions, construyendo un verificador (verificado). | [pdf] | Clase07.WP.fst |
| - | 16/10 | Suspendida por las Gloriosas JCC | ||
| - | 23/10 | Suspendida | ||
| 8 | 30/10 | Efectos en F* y verificación, Mónadas de Dijkstra. | [pdf] | Clase08.Eff.fst (ver repositorio para Makefile y archivos de Dune). |
| 06/11 | Clase invitada: Nikolaj Bjørner | [pdf] |
Repositorio Z3 Guía Z3 Programando Z3 |
|
| 9 | 20/11 | Introducción a lógica de separación | [pdf] | Clase09.fst |
| 10 | 27/11 | Permisos fraccionales e invariantes en SL | [pdf] | Clase10.fst |
| 11 | 04/12 | Pruebas calculacionales. Clases de tipo. | [pdf] | Clase11.Calc.fst Clase11.DEQ.fst Container.fst Clase11.Cliente.fst Clase11.Listas.fst Clase11.Listas.fsti |
| 12 | 11/12 | Clase invitada: Tahina Ramananandro sobre EverParse. Cierre. | [pdf] [pptx] | |