Nivel 5

El cubo-λ

Tres formas de dependencia (λ2, λω̲, λP) y su combinación en el Cálculo de Construcciones.

Adaptado de: Capítulo: El cubo-λ y su conexión al CIC.

Contenido

1. λ2: polimorfismo
2. λω̲: constructores de tipos
3. λP: tipos dependientes
4. El cubo completo
5. Propiedades metateóricas