Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
teaching:cc5104 [2010/07/15 11:21] – etanter | teaching:cc5104 [2014/05/30 08:44] – etanter | ||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== CC5104/ | ||
+ | **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, | ||
+ | |||
+ | **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), | ||
+ | * 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.// | ||
+ | |||
+ | **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, | ||
+ | * conexión con lógica constructiva (o " | ||
+ | * polimorfismo de subtipos, coerciones | ||
+ | * tipear objetos (object calculus, Featherweight Java) | ||
+ | * polimorfismo paramétrico (" | ||
+ | * inferencia de tipos | ||
+ | * el debate " | ||
+ | * perspectivas en verificación de software: sistemas de tipos y efectos, analisis de programa, model checking, theorem proving, etc. | ||
+ | |||
+ | Además de la base teorica, el curso insistirá sobre la construcción de artefactos (en particular type checkers). | ||
+ | |||
+ | ** Material de referencia** | ||
+ | * **(principalmente)** Types and Programming Languages (TAPL), Benjamin Pierce | ||
+ | * 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/ | ||
+ | |||
+ | ** Evaluación ** | ||
+ | |||
+ | Mini-controles y tareas. No hay examen. |