Cálculo de Construcciones

El Cálculo de Construcciones (CoC) es un lambda-cálculo tipificado de alto nivel que contiene un álgebra de tipos. CoC permite definir funciones por ejemplo, de enteros en tipos, de tipos en tipos al igual que las funciones de enteros en enteros. El cálculo de construcciones tiene la propiedad de normalización fuerte. El desarrollador inicial de CoC fue Thierry Coquand en el INRIA, Francia.El cálculo de construcciones sirvió de base a las primeras versiones del demostrador de teoremas Coq; las versiones posteriores se construyeron sobre el cálculo de Construcciones Inductivas que es una extensión de CoC con soporte para tipos de datos inductivos. En el CoC original, los tipos inductivos debían ser emulados con otras construcciones del cálculo.