Cálculo de Construcciones
- Cálculo de Construcciones
-
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.
Categoría: Demostradores de teoremas
Wikimedia foundation.
2010.
Mira otros diccionarios:
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 fuciones de enteros en enteros.… … Enciclopedia Universal
Teoría de tipos — Este artículo o sección necesita referencias que aparezcan en una publicación acreditada, como revistas especializadas, monografías, prensa diaria o páginas de Internet fidedignas. Puedes añadirlas así o avisar … Wikipedia Español
Coq — Saltar a navegación, búsqueda Coq (gallo en francés) es un sistema de ayuda para la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar pruebas para esas aserciones y… … Wikipedia Español
Coq — (gallo en francés) es un sistema de ayuda a la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar prubas para esas aserciones y extrae programas certificados (correctos) … Enciclopedia Universal
Empirismo — Saltar a navegación, búsqueda … Wikipedia Español
Teotihuacan — Altépetl mesoamericano Vista de la calzada de los Muertos desde la Pirámide de la Luna … Wikipedia Español
Galpón — Un galpón en Wisconsin. Se denomina galpón a una construcción relativamente grande que suele destinarse al depósito de mercaderías o maquinarias. Suelen ser construcciones rurales con una sola puerta. Contenido 1 … Wikipedia Español
Ingeniería civil — Áreas del saber física, química, cálculo, geografía y geología Campo de aplicación infraestructuras, obras hidráulicas y de transporte, constructoras, hidroeléctricas y centrales térmicas, siderometalúrgicas, asesoría y consultoría, urbanismo … Wikipedia Español
Número real — Diferentes clases de números reales. Recta real … Wikipedia Español
E8 (matemáticas) — Saltar a navegación, búsqueda En matemática, es el nombre de un grupo de Lie (el más grande) simple y excepcional y del álgebra de Lie que le está asociada. Su álgebra de Lie es formulada con la notación . La estructura E8 fue descubierta en 1887 … Wikipedia Español
