| Fecha | Tema | Referencia | Adicional | |
|---|---|---|---|---|
| M 30 Jul | introducción | - | articulo sobre tipos | |
| L 4 Ago | semántica via sintaxis | SEwPR Cap 1 | - | |
| M 6 Ago | analizar semántica (intro) | SEwPR Cap 2 | - | |
| intro a PLT Redex | SEwPR Cap 11 | bool1.rkt | ||
| L 11 Ago | analizar semántica | SEwPR Cap 2 | - | |
| redex-check | SEwPR Cap 14 | bool2.rkt | ||
| M 13 Ago | contextos de evaluación | bool3.rkt | Run your research! | |
| L 18 Ago | lambda calculo | SEwPR Cap 3 | lc1.rkt | |
| M 20 Ago | paro | |||
| L 25 Ago | lambda calculo | SEwPR Cap 3 | control 1 | |
| M 27 Ago | repaso control 1 | |||
| fin lambda calculo | SEwPR Cap 3 | |||
| 1/3 Sep | profe en conferencia – no hay clase | |||
| tarea: estudiar el capitulo 3 hasta 3.7 incluido, experimentando con Redex | ||||
| L 8 Sep | ISWIM | SEwPR Cap 4 | ||
| L 10 Sep | ISWIM: reducción estándar | SEwPR Cap 5 | ||
| 15/17 Sep | vacaciones fiestas patrias | |||
| L 22 Sep | Errores | SEwPR Cap 8.1-8.2 | ||
| M 24 Sep | Excepciones y continuaciones | SEwPR Cap 8.3-8.5 | Tarea 2 | |
| L 29 Sep | Intro tipos | terminology.pdf | Type systems, L. Cardelli | |
| Aritmética con tipos | TAPL Cap 8.1-8.2 | typed-arithm1.pdf | ||
| M 1 Oct | Aritmética con tipos: consistencia | TAPL Cap 8.3 | typed-arithm2.pdf | |
| control 2 | ||||
| L 6 Oct | Lambda calculo con tipos simples: | TAPL Cap 9.1-9-3 | stlc-progress.pdf | |
| definición y progreso | SEwPR Cap 10 | |||
| M 8 Oct | Lambda calculo con tipos simples: preservación | TAPL Cap 9 | stlc-preservation.pdf | |
| control 3a | ||||
| L 13 Oct | Extensiones simples | TAPL 11.1-11.8 | extensions.pdf | |
| M 15 Oct | Tipos universales | TAPL 23 | universals.pdf | |
| 20/22 Oct | profe en conferencia – no hay clase | |||
| L 27 Oct | Tipos existenciales | TAPL 24 | existentials.pdf | |
| Trailer: subtipos | TAPL 15 | subtyping.pdf | ||
| M 29 Oct | Tipos graduales | gradual.pdf | siek-gradual.pdf | |
| L 3 Nov | Lógica proposicional y deducción natural | natded.pdf | ||
| Curry-Howard: proposiciones como tipos | pap.pdf | wadler-pat.pdf | ||
| M 5 Nov | Lambda-cube | |||
| Intro a Coq | vectors.v | |||
| 10/12 Nov | estudio personal: capítulos Basics, Induction, Lists, Poly, Logic del Software Foundations | |||
| L 17 Nov | Interprete de expresiones y máquina de stack en Coq | CPDT 2.1 | cc71-1.v | |
| M 19 Nov | Compilador y demostración de correctitud | CPDT 2.1 | cc71-2.v | |
| M 3 Dec | Mini-conferencia | |||
Referencias: