Calculus of constructions (original) (raw)
In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants. Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity).
| Property | Value |
|---|---|
| dbo:abstract | In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants. Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity). (en) El Cálculo de Construcciones (CoC) es un 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 . El desarrollador inicial de CoC fue 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. * Datos: Q858320 (es) 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. La façon de définir le calcul des constructions par trois types de dépendances est appelée le lambda cube et est due à Henk Barendregt. (fr) Исчисление конструкций (англ. calculus of constructions, CoC) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — . Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики. Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе ). Среди вариантов исчисления — исчисление индуктивных конструкций (использует индуктивные типы), исчисление коиндуктивных конструкций (с применением коиндукции), предикативное исчисление индуктивных конструкций (устраняет некоторую часть непредикативности). С точки зрения соответствия Карри — Ховарда исчисление конструкций устанавливает взаимосвязь между зависимыми типами и доказательствами в секвенциальном интуиционистском исчислении предикатов. (ru) 构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。 (zh) |
| dbo:wikiPageExternalLink | http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf http://yquem.inria.fr/~huet/PUBLIC/induction.pdf http://hal.archives-ouvertes.fr/docs/00/07/60/24/PDF/RR-0530.pdf https://web.archive.org/web/20140529103535/http:/www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf https://web.archive.org/web/20150701130220/http:/yquem.inria.fr/~huet/PUBLIC/induction.pdf%7Carchive-date=2015-07-01 http://hal.inria.fr/inria-00076024/en/ |
| dbo:wikiPageID | 613557 (xsd:integer) |
| dbo:wikiPageLength | 9574 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1090953725 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Proof_assistant dbr:Typed_lambda_calculus dbr:Dependent_type dbc:Lambda_calculus dbr:Homotopy_type_theory dbr:Intuitionistic_logic dbr:Intuitionistic_type_theory dbr:Consistent dbr:Coq dbr:Mathematical_logic dbr:Coinduction dbr:Computer_science dbr:Henk_Barendregt dbr:Pure_type_system dbr:Matita dbr:Backus–Naur_form dbr:Type_theory dbr:Lambda_cube dbc:Dependently_typed_programming dbr:Church_encoding dbr:Foundations_of_mathematics dbr:Gödel's_incompleteness_theorem dbr:Thierry_Coquand dbc:Type_theory dbr:System_F dbr:Constructivism_(mathematics) dbr:Normalization_property_(lambda-calculus) dbr:Curry–Howard_isomorphism |
| dbp:wikiPageUsesTemplate | dbt:Cite_techreport dbt:Cite_book dbt:Cite_document dbt:Cite_journal dbt:Cite_web dbt:Cn dbt:Refbegin dbt:Refend dbt:Reflist dbt:Short_description |
| dct:subject | dbc:Lambda_calculus dbc:Dependently_typed_programming dbc:Type_theory |
| gold:hypernym | dbr:Theory |
| rdf:type | dbo:Work |
| rdfs:comment | In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants. Some of its variants include the calculus of inductive constructions (which adds inductive types), the calculus of (co)inductive constructions (which adds coinduction), and the predicative calculus of inductive constructions (which removes some impredicativity). (en) 构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。 (zh) El Cálculo de Construcciones (CoC) es un 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 . El desarrollador inicial de CoC fue en el INRIA, Francia. * Datos: Q858320 (es) 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. (fr) Исчисление конструкций (англ. calculus of constructions, CoC) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — . Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики. Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе ). (ru) |
| rdfs:label | Cálculo de Construcciones (es) Calculus of constructions (en) Calcul des constructions (fr) Исчисление конструкций (ru) 构造演算 (zh) |
| owl:sameAs | freebase:Calculus of constructions wikidata:Calculus of constructions dbpedia-es:Calculus of constructions dbpedia-fr:Calculus of constructions dbpedia-ru:Calculus of constructions dbpedia-zh:Calculus of constructions https://global.dbpedia.org/id/51axk |
| prov:wasDerivedFrom | wikipedia-en:Calculus_of_constructions?oldid=1090953725&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Calculus_of_constructions |
| is dbo:wikiPageDisambiguates of | dbr:COC |
| is dbo:wikiPageRedirects of | dbr:Calculus_of_Constructions dbr:Calculus_of_Inductive_Constructions dbr:Calculus_of_inductive_constructions |
| is dbo:wikiPageWikiLink of | dbr:Calculus_of_Constructions dbr:List_of_functional_programming_topics dbr:Typed_lambda_calculus dbr:Dependent_type dbr:Homotopy_type_theory dbr:Per_Martin-Löf dbr:Intuitionistic_type_theory dbr:List_of_mathematical_logic_topics dbr:Coq dbr:Normal_form_(abstract_rewriting) dbr:Constructive_proof dbr:Pure_type_system dbr:Type_theory dbr:Lambda_cube dbr:List_object dbr:Minimal_logic dbr:History_of_type_theory dbr:Natural_deduction dbr:Gérard_Huet dbr:Thierry_Coquand dbr:Lambda_calculus dbr:Lean_(proof_assistant) dbr:COC dbr:Calculus_of_Inductive_Constructions dbr:Calculus_of_inductive_constructions dbr:Meta-circular_evaluator |
| is foaf:primaryTopic of | wikipedia-en:Calculus_of_constructions |