Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Last revisionBoth sides next revision
teaching:cc5104 [2014/05/30 08:42] – etanterteaching:cc5104 [2014/05/30 08:47] – etanter
Line 7: Line 7:
 **Nota** **Nota**
 La nueva edición del curso tendrá dos enfoques adicionales:  La nueva edición del curso tendrá dos enfoques adicionales: 
-    * tipos graduales adoptados bajo alguna variante en los recientes lenguajes Dart (Google), TypeScript (Microsoft), Hack (Facebook), etc.)  +    * **tipos graduales**: combinar tipos estáticos y dinámicos. Tipos graduales fueron adoptados bajo alguna variante en los recientes lenguajes Dart (Google), TypeScript (Microsoft), Hack (Facebook), etc.)  
-    * introducción a la programación certificada en Coq+    * introducción a la **programación certificada** en Coq: definir programas junto con una demostración de su correctitud.
  
  
Line 23: Line 23:
    * simples extensiones (formas derivadas, pares, tuplas, records, sumas, variantes, etc.)    * simples extensiones (formas derivadas, pares, tuplas, records, sumas, variantes, etc.)
    * extensiones avanzadas: recursión, referencias, excepciones    * 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")    * polimorfismo paramétrico ("generics")
    * inferencia de tipos    * 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** ** Material de referencia**
    * **(principalmente)** Types and Programming Languages (TAPL), Benjamin Pierce    * **(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    * Programming Languages: Application and Interpretation (PLAI), Shriram Krishnamurthi
    * Practical Foundations for Programming Languages (PFPL), Robert Harper    * 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 ** ** Evaluación **
  
 Mini-controles y tareas. No hay examen. Mini-controles y tareas. No hay examen.
 +
 +** Horario **
 +
 +TBA
 +