CC71Y - Lenguajes de Programación II

Objetivo general

El curso entrega los elementos técnicos y formales necesarios para entender la problemática 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, demostrando 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.

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.

Contenidos

  • semántica de lenguajes, lambda calculus
  • sistemas de tipos estáticos y dinámicos
  • lenguajes seguro y sistemas de tipos coherentes
  • el Halting Problem, tipos y contratos
  • simply-typed lambda calculus
  • simples extensiones (formas derivadas, pares, tuplas, records, sumas, variantes, etc.)
  • extensiones avanzadas: recursión, referencias, excepciones
  • polimorfismo paramétrico (“generics”)
  • inferencia de tipos
  • conexión con lógica constructiva (o “propositions as types”)
  • polimorfismo de subtipos, coerciones
  • tipos graduales
  • tipos dependientes y programación certificada.

Además de la base teórica, el curso insistirá sobre la construcción de artefactos.

Material de referencia

  • Types and Programming Languages (TAPL), Benjamin Pierce. MIT Press.
  • Semantics Engineering with PLT Redex, Matthias Felleisen et al. MIT Press.
  • Practical Foundations for Programming Languages (PFPL), Robert Harper. MIT Press.
  • Software Foundations (SF), B. Pierce et al. Online.
  • Certified Programming with Dependent Types (CPDT), Adam Chlipala. MIT Press.
  • Programming Languages: Application and Interpretation (PLAI), Shriram Krishnamurthi. Online.

Evaluación

Mini-controles y tareas. No hay examen.

El curso termina con una mini-conferencia donde los estudiantes presentan temas estudiados en base a artículos y/o capítulos de libros.

Horario

Por definir (dos bloques por semana).