Introducción: notación deductiva, inducción sobre derivaciones, cálculo lambda con tipos simples.
Lenguaje funcional básico y correspondencia Curry-Howard.
Polimorfismo
Tipos de Refinamiento
Tipos Dependientes
Tipos Graduales
80% tareas teórico-prácticas (más teóricas que prácticas)
20% actividades (lecturas y posible exposición en clase)
No hay reposición de ninguno de los anteriores, ni hay examen final.
Para tener derecho a calificación final aprobatoria es necesario tener un promedio aprobatorio de tareas.
Para obtener un NP es necesario que no se tengan más de dos calificaciones de cualquier tipo.