The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.

PropertyValue
dbpprop:abstract
  • The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.
  • 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.
  • Le calcul des constructions (CoC de l'anglais calculus of constructions) est un lambda-calcul typé d'ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions qui vont des entiers vers les entiers, mais aussi des entiers vers les types ou des types vers les types. Le CoC est fortement normalisant, bien que, d'après le théorème d'incomplétude de Gödel, il soit impossible de démontrer cette propriété dans le CoC lui-même, puisqu'elle implique sa cohérence. Le CoC a été développé initialement par Thierry Coquand. Le CoC a été à l'origine des premières versions de l'assistant de preuves Coq. Les versions suivantes ont été construites à partir du calcul des constructions inductives qui est une extension du CoC qui intègre des types de données inductives. Dans le CoC originel, les types de données inductives devaient être émulés à l'aide de leur fonction de destruction.
  • 构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 Thierry Coquand 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。
dbpprop:date
  • November 2008
dbpprop:hasPhotoCollection
dbpprop:reference
dbpprop:wikiPageUsesTemplate
rdfs:comment
  • The calculus of constructions (CoC) is a formal language in which both computer programs and mathematical proofs can be expressed. This language forms the basis of theory behind the Coq proof assistant, which implements the derivative calculus of inductive constructions.
  • 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.
  • Le calcul des constructions (CoC de l'anglais calculus of constructions) est un lambda-calcul typé d'ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions qui vont des entiers vers les entiers, mais aussi des entiers vers les types ou des types vers les types.
rdfs:label
  • Calculus of constructions
  • Cálculo de Construcciones
  • Calcul des constructions
  • 构造演算
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of