Programa de Asignatura

Ingeniería en Computación - In.Co.
Nombre de la Asignatura Construcción Formal de Programas en Teoría de Tipos.
Créditos 12
Objetivo de la Asignatura Iniciar al estudiante al uso de métodos formales para la producción de software correcto por construcción.
Metodología de enseñanza CARGA TOTAL DE TRABAJO: 
180 horas. 
Horas de aula semanales: 6 
Horas de trabajo del estudiante semanales: 6 

Se dictarán clases teóricas, prácticas y de laboratorio en máquinas. 
Se utilizará como asistente de pruebas el sistema Coq.
Temario 1.Asistentes de pruebas para lógicos y matemáticos: Una presentación formal de la lógica proposicional y de primer orden. 
2.Asistentes de Pruebas para programadores: El calculo lambda como lenguaje de programación funcional. 
3.Identificacion de pruebas y programas: Isomorfismo de Curry Howard 
4.Recursion: Definiciones Inductivas, Principios de Inducción, Esquemas de Recursión. 
5.Extraccion de programas a partir de pruebas. Construcción de Pruebas a partir de programas. 
6.Construccion de programas certificados usando Coq.
Bibliografía Interactive Theorem Proving and Program Development.
Y. Bertot, P. Casteran
Springer-Verlag, 2004.

Computation and Reasoning: A Type Theory for Computer Science. Volume 11 of International Series of Monographs on Computer Science. Oxford Science Publications, 1994. ISBN: 0198538359 

The Coq Proof Assistant. Reference Manual. B. Barras et al. Rapport de Recherche INRIA. Disponible en: 
http://pauillac.inria.fr/coq/doc-eng.html

A Tutorial on Recursive Types in Coq. Eduardo Giménez, Rapport de Recherche INRIA. Disponible en: 
http://pauillac.inria.fr/coq/doc-eng.html
Conocimientos previos exigidos y recomendados Cálculo Proposicional y de Predicados. Deducción natural. Conjuntos y pruebas inductivas.
Cálculos funcionales. Funciones de alto orden. Sistemas de Tipos. Programación Funcional.
Programación Lógica, procedimientos de unificación de términos.
  Anexo:

La asignatura se evaluará por medio de dos parciales y trabajos de laboratorio. El nivel mínimo de suficiencia en los trabajos de laboratorio es eliminatorio, ya que esta parte del trabajo del curso no puede ser evaluada mediante exámenes. Por otra parte, dependiendo de las condiciones de dictado del curso, el trabajo de laboratorio se evalúa según las opciones aprobado/no aprobado, o con puntaje diferenciado en el caso de aprobación. En este último caso, el puntaje del laboratorio se integraría al puntaje total del curso, prorrateándose en los de las pruebas parciales.

En todos los casos de los resultados obtenidos surgen dos posibilidades:

- Exoneración del curso

- Insuficiencia en el curso; el estudiante reprueba el curso

Se presenta a continuación el esquema de evaluación del curso

Exoneración. El estudiante debe cumplir los siguientes requisitos :

  
Insuficiencia. El estudiante no obtiene los puntajes de ninguna de las franjas anteriores.                Plan 87: Lógica (E-C)
               Plan 97:
                   - Lógica (E-C)
              - Introducción a la Programación Funcional (E-C) o
                     Electiva Lógica (E-C) (Introducción a la Programación Lógica o Programación Lógica )