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
teaching:cc5104 [2011/10/08 20:17] – etanterteaching:cc5104 [2014/05/30 11:48] (current) – etanter
Line 1: Line 1:
-====== CC5104/CC71Y - Lenguajes de Programación II  ======+====== CC71Y - Lenguajes de Programación II  ======
  
 **Objetivo general** **Objetivo general**
  
 El curso entrega los elementos técnicos y formales necesarios para entender la problematica de garantizar que los programas cumplen con sus objetivos, limitando efectos indeseados, lo más temprano posible. Se estudian las nociones de programas válidos, errores y excepciones, contratos, y sobre todo, tipos. En particular, se describen los conceptos fundamentales de los sistemas de tipos, permitiendo entender porque los lenguajes de hoy siguen evolucionando en ese aspecto (por ejemplo, el sistema de tipos de Java), y porque no existe una respuesta única y definitiva al problema. El alumno será capaz además de relacionar un sistema de tipo con la semántica del lenguaje, probando su coherencia. Además de proveer un entendimiento más profundo de los lenguajes de programación, el curso habilita a los alumnos para diseñar (extensiones de) lenguajes que proveen garantías fuertes de buen comportamiento. El curso entrega los elementos técnicos y formales necesarios para entender la problematica de garantizar que los programas cumplen con sus objetivos, limitando efectos indeseados, lo más temprano posible. Se estudian las nociones de programas válidos, errores y excepciones, contratos, y sobre todo, tipos. En particular, se describen los conceptos fundamentales de los sistemas de tipos, permitiendo entender porque los lenguajes de hoy siguen evolucionando en ese aspecto (por ejemplo, el sistema de tipos de Java), y porque no existe una respuesta única y definitiva al problema. El alumno será capaz además de relacionar un sistema de tipo con la semántica del lenguaje, probando su coherencia. Además de proveer un entendimiento más profundo de los lenguajes de programación, el curso habilita a los alumnos para diseñar (extensiones de) lenguajes que proveen garantías fuertes de buen comportamiento.
 +
 +**Nota:**
 +La nueva edición del curso tendrá dos enfoques adicionales: 
 +    * **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: definir programas junto con una demostración de su correctitud.
 +
 +
  
 //Este curso es parte de los grupos de cursos recomendados para las lineas de especialización en Ciencia de la Computación y en Ingeniería de Software.// //Este curso es parte de los grupos de cursos recomendados para las lineas de especialización en Ciencia de la Computación y en Ingeniería de Software.//
Line 16: 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
 +