Página del curso

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.rktRun 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.5Tarea 2
L 29 Sep Intro tipos terminology.pdfType systems, L. Cardelli
Aritmética con tiposTAPL Cap 8.1-8.2typed-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 9stlc-preservation.pdf
control 3a
L 13 Oct Extensiones simples TAPL 11.1-11.8extensions.pdf
M 15 Oct Tipos universalesTAPL 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.pdfsiek-gradual.pdf
L 3 Nov Lógica proposicional y deducción naturalnatded.pdf
Curry-Howard: proposiciones como tipospap.pdfwadler-pat.pdf
M 5 Nov Lambda-cube
Intro a Coqvectors.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 CoqCPDT 2.1cc71-1.v
M 19 Nov Compilador y demostración de correctitudCPDT 2.1cc71-2.v
M 3 Dec Mini-conferencia

Referencias: