Math 2.0

Mathematical logic and foundations Concept

Calculus of constructions

Builds on System FDependent typeLambda cube

Summary

The calculus of constructions is a typed lambda calculus introduced by Thierry Coquand and Gérard Huet. It combines the polymorphism of System F, type operators, and dependent types in one system, and it sits at the top of Barendregt's lambda cube. It is strongly normalizing, and as a logic it is a higher-order intuitionistic logic in which proofs are terms. With inductive types added it became the basis of the proof assistant Coq, now called Rocq.

Reading path

To understand this page from the ground up, read these 27 pages in order. The foundations come first.

Show the path as a graph
Element, definition, no evidence levelElementdefinitionIntuitionistic logic, concept, no evidence levelIntuitionistic logicconceptLambda calculus, concept, no evidence levelLambda calculusconceptLambda cube, concept, no evidence levelLambda cubeconceptProposition, concept, no evidence levelPropositionconceptSet, concept, no evidence levelSetconceptSet, definition, no evidence levelSetdefinitionConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionTruth table, concept, no evidence levelTruth tableconceptModus ponens, concept, no evidence levelModus ponensconceptMathematical proof, concept, no evidence levelMathematical proofconceptPropositional logic, concept, no evidence levelPropositional logicconceptTautology, definition, no evidence levelTautologydefinitionLogical equivalence, definition, no evidence levelLogical equivalencedefinitionDouble negation law, statement, no evidence levelDouble negation lawstatementProof by contradiction, concept, no evidence levelProof by contradictionconceptRussell's paradox, statement, no evidence levelRussell's paradoxstatementType theory, concept, no evidence levelType theoryconceptCurry–Howard correspondence, concept, no evidence levelCurry–Howard correspo…conceptDependent type, concept, no evidence levelDependent typeconceptSimply typed lambda calculus, concept, no evidence levelSimply typed lambda c…conceptSystem F, concept, no evidence levelSystem FconceptCalculus of constructions, concept, no evidence levelCalculus of construct…concept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Element definition
  2. Intuitionistic logic concept
  3. Lambda calculus concept
  4. Lambda cube concept
  5. Proposition concept
  6. Set concept
  7. Set definition
  8. Conjunction definition
  9. Disjunction definition
  10. Implication definition
  11. Negation definition
  12. Biconditional definition
  13. Truth table concept
  14. Modus ponens concept
  15. Mathematical proof concept
  16. Propositional logic concept
  17. Tautology definition
  18. Logical equivalence definition
  19. Double negation law statement
  20. Proof by contradiction concept
  21. Russell's paradox statement
  22. Type theory concept
  23. Curry–Howard correspondence concept
  24. Dependent type concept
  25. Simply typed lambda calculus concept
  26. System F concept
  27. Calculus of constructions concept

Where this leads

3 pages build on this one.

Further reading

  1. Web https://en.wikipedia.org/wiki/Calculus_of_constructions
About this page
TagTKMY3F6KSA
URIm2://TKMY3F6KSA
Kindconcept
WritingW0 stub
MSC03B38, 03B40, 68V15
UsesSystem F, Dependent type, Lambda cube
Same as
Changed3 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Definitions

Used by