Differences

This shows you the differences between two versions of the page.

--- teaching:cc5104 [2014/05/30 08:44] – etanter
+++ teaching:cc5104 [2014/05/30 08:47] – etanter
@@ Line 23: / Line 23: @@
    * simples extensiones (formas derivadas, pares, tuplas, records, sumas, variantes, etc.)
    * extensiones avanzadas: recursión, referencias, excepciones
-   * conexión con lógica constructiva (o "propositions as types")
-   * polimorfismo de subtipos, coerciones
-   * tipear objetos (object calculus, Featherweight Java)
    * polimorfismo paramétrico ("generics")
    * inferencia de tipos
-   * el debate "dynamic vs. static typing"
+   * conexión con lógica constructiva (o "propositions as types")
-   * perspectivas en verificación de software: sistemas de tipos y efectos, analisis de programa, model checking, theorem proving, etc.
+   * polimorfismo de subtipos, coerciones
+   * tipos graduales
+   * tipos dependientes y programación certificada.
-Además de la base teorica, el curso insistirá sobre la construcción de artefactos (en particular type checkers).
+Además de la base teorica, el curso insistirá sobre la construcción de artefactos.
 ** Material de referencia**
    * **(principalmente)** Types and Programming Languages (TAPL), Benjamin Pierce
+   * Software Foundations (SF), B. Pierce et al.
+   * Certified Programming with Dependent Types (CPDT), Adam Chlipala
    * Programming Languages: Application and Interpretation (PLAI), Shriram Krishnamurthi
    * Practical Foundations for Programming Languages (PFPL), Robert Harper
-   * Type Systems (TS), Luca Cardelli
-** Horario **
-Para el 2011/2, el horario es: 1.5/2.5
 ** Evaluación **
 Mini-controles y tareas. No hay examen.
+** Horario **
+TBA