Cálculo de Construcciones
De Wikipedia, la enciclopedia libre
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 le 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.
El contenido de esta página es un esbozo sobre matemática. Ampliándolo ayudarás a mejorar Wikipedia.
Puedes ayudarte con las wikipedias en otras lenguas.
