papers.yml

papers:
  - title: "The Coq Proof Assistant Version 8.20.0"
    publication: Zenodo
    abstract: >
      Coq version 8.20 adds a new rewrite rule mechanism along with a few new features, a host of improvements to the virtual machine, the notation system, Ltac2 and the standard library.
    authors: 
      - Yves Bertot
      - Frédéric Besson
      - Ana Borges
      - Ali Caglayan 
      - Tej Chajed
      - Cyril Cohen
      - Pierre Corbineau
      - Pierre Courtieu
      - Andres Erbsen
      - Jim Fehrle
      - Julien Forest
      - Emilio Jesús Gallego Arias
      - Gaëtan Gilbert
      - Georges Gonthier
      - Benjamin Grégoire
      - Jason Gross
      - Hugo Herbelin
      - Vincent Laporte
      - Olivier Laurent
      - Assia Mahboubi
      - Kenji Maillard
      - Erik Martin-Dorel
      - Guillaume Melquiond
      - Pierre-Marie Pédrot
      - Clément Pit-Claudel
      - Pierre Roux
      - Kazuhiko Sakaguchi
      - Vincent Semeria
      - Michael Soegtrop
      - Matthieu Sozeau
      - Arnaud Spiwack
      - Nicolas Tabareau
      - Enrico Tassi
      - Laurent Théry
      - Anton Trunov
      - Xia Li-yao
      - Théo Zimmermann
    year: 2024
    tags:
      - Theory and Implementation of Rocq
      - Release
    links:
      - description: "Zenodo"
        uri: "https://zenodo.org/records/14542673"
    featured: true

  - title: "Verified Extraction from Coq to OCaml"
    publication: Programming Language Design and Implementation (PLDI)
    abstract: >
      One of the central claims of fame of the Coq proof assistant is extraction, i.e., the ability to obtain efficient programs in industrial programming languages such as OCaml, Haskell, or Scheme from programs written in Coq's expressive dependent type theory. Extraction is of great practical usefulness, used crucially e.g., in the CompCert project. However, for such executables obtained by extraction, the extraction process is part of the trusted code base (TCB), as are Coq's kernel and the compiler used to compile the extracted code. The extraction process contains intricate semantic transformation of programs that rely on subtle operational features of both the source and target language. Its code has also evolved since the last theoretical exposition in the seminal PhD thesis of Pierre Letouzey. Furthermore, while the exact correctness statements for the execution of extracted code are described clearly in academic literature, the interoperability with unverified code has never been investigated formally, and yet is used in virtually every project relying on extraction. In this paper, we describe the development of a novel extraction pipeline from Coq to OCaml, implemented and verified in Coq itself, with a clear correctness theorem and guarantees for safe interoperability. We build our work on the MetaCoq project, which aims at decreasing the TCB of Coq's kernel by reimplementing it in Coq itself and proving it correct w.r.t. a formal specification of Coq's type theory in Coq. Since OCaml does not have a formal specification, we make use of the Malfunction project specifying the semantics of the intermediate language of the OCaml compiler. Our work fills some gaps in the literature and highlights important differences between the operational semantics of Coq programs and their extracted variants. In particular, we focus on the guarantees that can be provided for interoperability with unverified code, identify guarantees that are infeasible to provide, and raise interesting open question regarding semantic guarantees that could be provided. As central result, we prove that extracted programs of first-order data type are correct and can safely interoperate, whereas for higher-order programs already simple interoperations can lead to incorrect behaviour and even outright segfaults.
    authors:
      - Yannick Forster 
      - Matthieu Sozeau
      - Nicolas Tabareau 
    tags:
      - Theory and Implementation of Rocq
      - PLDI
      - extraction
    year: 2024
    links:
      - description: "ACM Digital Library"
        uri: https://dl.acm.org/doi/10.1145/3656379
      - description: "HAL-Inria"
        uri: https://inria.hal.science/hal-04329663/
      - description: "PLDI Talk"
        uri: "https://youtu.be/RBU3dkSv7rg?list=PLyrlk8Xaylp6XYPbTIscsn49yFEFlxUp-&t=11946"
    featured: true

  - title: "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq"
    publication: Journal of the ACM
    abstract: >
      Coq is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system, template polymorphism and η-conversion), which is proven sound and complete in Coq with respect to its formal specification. Note that because of Gödel’s second incompleteness theorem, there is no hope to prove completely the soundness of the specification of Coq inside Coq (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the MetaCoq project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq. It is worth mentioning that during the verification process, we have found a source of incompleteness in Coq’s official type checker, which has then been fixed in Coq 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of Coq is the so-called extraction mechanism: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for Coq in the future.
    authors:
      - Matthieu Sozeau
      - Yannick Forster
      - Meven Lennon-Bertrand
      - Jakob Botsch Nielsen
      - Nicolas Tabareau
      - Théo Winterhalter
    tags:
      - Theory and Implementation of Rocq
      - JACM
      - type-checker
    year: 2024
    links:
      - description: "Journal of the ACM"
        uri: https://dl.acm.org/doi/10.1145/3706056
      - description: "HAL-Inria"
        uri: https://inria.hal.science/hal-04077552
    featured: true

  - title: "Trocq: Proof Transfer for Free, With or Without Univalence"
    publication: European Symposium on Programming
    abstract: >
      In interactive theorem proving, a range of different representations may be available for a single mathematical concept, and some proofs may rely on several representations. Without automated support such as proof transfer, theorems available with different representations cannot be combined, without light to major manual input from the user. Tools with such a purpose exist, but in proof assistants based on dependent type theory, it still requires human effort to prove transfer, whereas it is obvious and often left implicit on paper. This paper presents Trocq, a new proof transfer framework, based on a generalization of the univalent parametricity translation, thanks to a new formulation of type equivalence. This translation takes care to avoid dependency on the axiom of univalence for transfers in a delimited class of statements, and may be used with relations that are not necessarily isomorphisms. We motivate and apply our framework on a set of examples designed to show that it unifies several existing proof transfer tools. The article also discusses an implementation of this translation for the Coq proof assistant, in the Coq-Elpi metalanguage.
    authors:
      - Cyril Cohen
      - Enzo Crance
      - Assia Mahboubi
    tags:
      - Theory and Implementation of Rocq
      - ESOP
      - Proof Transfer
    year: 2024
    links:
      - description: "HAL-Inria"
        uri: https://inria.hal.science/hal-04177913v5
    featured: true

  - title: "Proof Repair across Type Equivalences"
    publication: Programming Language Design and Implementation (PLDI)
    abstract: >
      We describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes.
      We have implemented this approach in PUMPKIN Pi, an extension to the PUMPKIN PATCH Coq plugin suite for proof repair. We demonstrate PUMPKIN Pi's flexibility on eight case studies, including supporting a benchmark from a user study, easing development with dependent types, porting functions and proofs between unary and binary numbers, and supporting an industrial proof engineer to interoperate between Coq and other verification tools more easily.
    authors:
      - Talia Ringer
      - RanDair Porter
      - Nathaniel Yazdani
      - John Leo
      - Dan Grossman
    tags:
      - Theory and Implementation of Rocq
      - PLDI
      - proof repair
    year: 2021
    links:
      - description: "ACM Digital Library"
        uri: https://dl.acm.org/doi/10.1145/3453483.3454033      
      - description: "Download PDF on Arxiv"
        uri: https://arxiv.org/abs/2010.00774
      - description: "PLDI Talk"
        uri: https://youtu.be/zG-Jc62WqFk?si=47mUgl_-RgvIGE71
    featured: no

  - title: "Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq"
    publication: International Conference on Functional Programming (ICFP)
    abstract: >
      Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.
    authors:
      - Matthieu Sozeau
      - Cyprien Mangin
    tags:
      - Theory and Implementation of Rocq
      - ICFP
      - Dependent pattern-matching
    year: 2019
    links:
      - description: "ACM Digital Library"
        uri: https://dl.acm.org/doi/10.1145/3341690
      - description: "Download PDF on Arxiv"
        uri: https://arxiv.org/abs/2010.00774
    featured: no

  - title: "Definitional Proof-Irrelevance without K"
    publication: Principles of Programming Languages (POPL)
    abstract: >
      Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory. Proof-irrelevance, stating that any two proofs of the same proposition are equal, is a possible way to extend conversion to make a type theory more powerful. However, this new power comes at a price if we integrate it naively, either by making type checking undecidable or by realizing new axioms—such as uniqueness of identity proofs (UIP)—that are incompatible with other extensions, such as univalence. In this paper, taking inspiration from homotopy type theory, we propose a general way to extend a type theory with definitional proof irrelevance, in a way that keeps type checking decidable and is compatible with univalence. We provide a new criterion to decide whether a proposition can be eliminated over a type (correcting and improving the so-called singleton elimination of Coq) by using techniques coming from recent development on dependent pattern matching without UIP. We show the generality of our approach by providing implementations for both Coq and Agda, both of which are planned to be integrated in future versions of those proof assistants.
    authors:
      - Gaëtan Gilbert
      - Jesper Cockx
      - Matthieu Sozeau
      - Nicolas Tabareau
    tags:
      - Theory and Implementation of Rocq
      - POPL
      - Proof-Irrelevance
    year: 2019
    links:
      - description: "ACM Digital Library"
        uri: https://dl.acm.org/doi/10.1145/3290316
      - description: "HAL-Inria"
        uri: https://inria.hal.science/hal-01859964
    featured: no

  - title: "Inductive Definitions in the System Coq - Rules and Properties"
    publication: Typed Lambda Calculi and Applications (TLCA)
    abstract: >
      In the pure Calculus of Constructions, it is possible to represent data structures and predicates using higher-order quantification. However, this representation is not satisfactory, from the point of view of both the efficiency of the underlying programs and the power of the logical system. For these reasons, the calculus was extended with a primitive notion of inductive definitions. This paper describes the rules for inductive definitions in the system Coq. They are general enough to be seen as one formulation of adding inductive definitions to a typed lambda-calculus. We prove strong normalization for a subsystem of Coq corresponding to the pure Calculus of Constructions plus Inductive Definitions with only weak eliminations.
    authors:
      - Christine Paulin-Mohring
    tags:
      - Theory and Implementation of Rocq
      - TLCA
      - Inductive types
    year: 1993
    links:
      - description: "DOI"
        uri: https://doi.org/10.1007/BFb0037116
    featured: no

  - title: "Inductively Defined Types"
    publication: International Conference on Computer Logic
    year: 1988
    page: 50-66
    authors:
      - Thierry Coquand
      - Christine Paulin-Mohring
    tags:
      - Theory and Implementation of Rocq
      - Inductive types
    links:
      - description: "DOI"
        uri: https://doi.org/10.5555/646125.758641
      - description: "Springer"
        uri: https://link.springer.com/content/pdf/10.1007/3-540-52335-9_47.pdf
    featured: no
    
  - authors:
      - family: Coquand
        given: Thierry
      - family: Huet
        given: Gérard
    container-title: Information and Computation
    doi: 10.1016/0890-5401(88)90005-3
    id: COQUAND88
    issue: 2
    issued: 1988
    page: 95-120
    title: The Calculus of Constructions
    type: article-journal
    volume: 76
    featured: no
    tags:
      - Theory and Implementation of Rocq
      - Foundations
    abstract: >
      The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a A-expression, typed
      with propositions of the underlying logic. By removing types we get a pure
      λ-expression, expressing its associated algorithm. Computing this
      λ-expression corresponds roughly to cut-elimination. It is our thesis that
      (as already advocated by Martin-Löf) the Curry-Howard correspondence between 
      propositions and types is a powerful paradigm for computer science. In the 
      case of constructions, we obtain the notion of a very highlevel functional 
      programming language, with complex polymorphism wellsuited for module specification. 
      The notion of type encompasses the usual notion of date type, but allows as well 
      arbitrarily complex algorithmic specifications. We develop the basic theory of a 
      calculus of constructions, and prove a strong normalization theorem showing that all
      computations terminate. Finally, we suggest various extensions to stronger calculi.
      
  - abstract: Type Classes have met a large success in Haskell and
      Isabelle, as a solution for sharing notations by overloading and for
      specifying with abstract structures by quantification on contexts.
      However, both systems are limited by second-class implementations of
      these constructs, and these limitations are only overcomed by ad-hoc
      extensions to the respective systems. We propose an embedding of
      type classes into a dependent type theory that is first-class and
      supports some of the most popular extensions right away. The
      implementation is correspondingly cheap, general and very well
      integrated inside the system, as we have experimented in Coq. We
      show how it can be used to help structured programming and proving
      by way of examples.
    author:
    - family: Sozeau
      given: Matthieu
    - family: Oury
      given: Nicolas
    tags:
      - Theory and Implementation of Rocq
    collection-title: LNCS
    container-title: TPHOLs
    doi: 10.1007/978-3-540-71067-7_23
    editor:
    - family: Otmane Ait Mohamed
      given: César Muñoz
    - family: Tahar
      given: Sofiène
    id: sozeau.Coq/classes/fctc
    issued: 2008
    keyword: Type classes
    page: 278-293
    publisher: Springer
    title: First-Class Type Classes
    type: paper-conference
    volume: 5170

  - author:
    - family: Poiret
      given: Josselin
    - family: Gilbert
      given: Gaëtan
    - family: Maillard
      given: Kenji
    - family: Pédrot
      given: Pierre-Marie
    - family: Sozeau
      given: Matthieu
    - family: Tabareau
      given: Nicolas
    - given: Éric
      family: Tanter
    container-title: POPL'25
    id: allyourbase
    issued: 2025
    note: To appear
    title: "All Your Base are Belong to Us: Sort Polymorphism for Proof
      Assistants"
    type: article-journal
    url: "https://nantes-universite.hal.science/hal-04801739"
    tags:
      - Theory and Implementation of Rocq
      - POPL
      - Universes
    abstract: >
      Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.
  
  - abstract: Motivated by applications to proof assistants based on
      dependent types, we develop and prove correct a strong reducer and
      β-equivalence checker for the λ-calculus with
      products, sums, and guarded fixpoints. Our approach is based on
      compilation to the bytecode of an abstract machine performing weak
      reductions on non-closed terms, derived with minimal modifications
      from the ZAM machine used in the Objective Caml bytecode
      interpreter, and complemented by a recursive "read back" procedure.
      An implementation in the Coq proof assistant demonstrates important
      speed-ups compared with the original interpreter-based
      implementation of strong reduction in Coq.
    author:
    - family: Grégoire
      given: Benjamin
    - family: Leroy
      given: Xavier
    tags:
      - Theory and Implementation of Rocq
    container-title: International Conference on Functional Programming
    id: Gregoire-Leroy-02
    issued: 2002
    page: 235-246
    publisher: ACM Press
    title: A compiled implementation of strong reduction
    type: paper-conference
    url: "http://pauillac.inria.fr/\\~xleroy/publi/strong-reduction.pdf"
    doi: 10.1145/581478.581501
  
  - author:
    - family: Dénès
      given: Maxime
    tags:
      - Theory and Implementation of Rocq
    id: "denes:tel-00945775"
    issued: 2013
    month: 11
    keyword: Formalized mathematics, Certified algorithms, Linear
      algebra, Formal proofs, Efficient verified computations, Homology
    number: 2013NICE4103
    publisher: Université Nice Sophia Antipolis
    title: "Étude formelle d'algorithmes efficaces en algèbre linéaire"
    type: thesis
    url: "https://theses.hal.science/tel-00945775"

  - author:
    - family: Letouzey
      given: Pierre
    tags: 
      - Theory and Implementation of Rocq
      - Extraction
    genre: Thèse de Doctorat
    id: LetouzeyPhd
    issued: 2004
    month: 7
    publisher: Université Paris-Sud
    title: "Programmation fonctionnelle certifiée: L'extraction de programmes dans l'assistant Coq"
    title-short: Programmation fonctionnelle certifiée
    type: thesis
    url: "http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf"

  - author: 
    - family: Timany
      given: Amin
    - family: Sozeau
      given: Matthieu
    collection-title: LIPIcs
    container-title: FSCD
    doi: 10.4230/LIPIcs.FSCD.2018.29
    editor:
    - family: Kirchner
      given: Hélène
    id: DBLP.conf/rta/TimanyS18
    isbn: 978-3-95977-077-4
    issued: 2018
    page: 1-16
    title: Cumulative Inductive Types in Coq
    type: paper-conference
    url: "https://doi.org/10.4230/LIPIcs.FSCD.2018.29"
    volume: 108
    tags: 
      - Theory and Implementation of Rocq
      - PCUIC
    abstract: >
      In order to avoid well-known paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type_0 : Type_1 : *s. Such type systems are called cumulative if for any type A we have that A : Type_i implies A : Type_{i+1}. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to formalization and definitional translations.
  
  - author:
    - family: Martin-Löf
      given: Per
    id: Martin-Lof-1972
    issued: 1972
    title: An Intuitionistic Theory of Types
    publisher: University of Stockholm
    url: https://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf
    tags:
      - Theory and Implementation of Rocq
      - MLTT
    abstract: >
      The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.      
  
  - author:
    - family: Girard
      given: J.-Y.
    genre: PhD thesis
    id: "Girard:1972fk"
    issued: 1972
    month: June
    publisher: Université Paris 7
    title: Interprétation fonctionnelle et élimination des coupures de
      l'arithmétique d'ordre supérieur
    type: thesis
    url: https://girard.perso.math.cnrs.fr/These.pdf
    tags:
      - Theory and Implementation of Rocq

  - author:
    - family: Whitehead
      given: Alfred North
    - family: Russell
      given: Bertrand
    issued: 1910
    publisher: Cambridge University Press
    title: Principia Mathematica
    tags:
      - Theory and Implementation of Rocq

  - author:
    - family: Paulin-Mohring
      given: Christine
    genre: PhD thesis
    id: "DBLP:phd/hal/PaulinMohring89"
    issued: 1989
    publisher: Paris Diderot University, France
    title: Extraction de programmes dans le calcul des constructions.
      (Program extraction in the calculus of constructions)
    type: thesis
    url: "https://tel.archives-ouvertes.fr/tel-00431825"
    tags: 
      - Theory and Implementation of Rocq

  - author:
    - family: Paulin-Mohring
      given: Christine
    title: Extracting Fω's Programs from Proofs in the Calculus of Constructions
    publication: ACM Symposium on Principles of Programming Languages
    location: Austin, Texas, USA
    month: January
    day: 11-13
    year: 1989
    pages: 89-104
    publisher: ACM Press
    doi: 10.1145/75277.75285
    abstract: >
      We define in this paper a notion of realizability for the Calculus of Constructions. The extracted programs are terms of the Calculus that do not contain dependent types. We introduce a distinction between informative and non-informative propositions. This distinction allows the removal of the “logical” part in the development of a program. We show also how to use our notion of realizability in order to interpret various axioms like the axiom of choice or the induction on integers. A practical example of development of program is given in the appendix.
    tags:
      - Theory and Implementation of Rocq

  - author:
    - family: Herbelin
      given: Hugo
    id: HerbelinUniverses
    issued: 2005
    publication: Manuscript
    title: Type Inference with Algebraic Universes in the Calculus of Inductive Constructions
    type: article-journal
    url: "http://pauillac.inria.fr/\\~herbelin/publis/univalgcci.pdf"
    abstract: >
      We describe an algebraic system of universes and a typechecking algorithm for universe constraints in a version of the extended calculus of constructions with inductive types. The use of algebraic universes ensures that the graph of constraints only contains universes already present in the term to type. This algorithm, used in the typechecker of the Coq proof assistant, refines Huet and Harper-Pollack algorithms for typical ambiguity.
    tags:
      - Theory and Implementation of Rocq

  - author:
    - family: Huet
      given: Gérard
    year: 1988
    publication: Unpublished draft
    title: Extending the Calculus of Constructions with Type:Type
    abstract: >
      The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn, Girard and Martin-Löf. The calculus and its syntactic theory were presented in Coquand’s thesis, and an implementation by the author was used to mechanically verify a substantial number of proofs demonstrating the power of expression of the formalism. The Calculus of Constructions is proposed as a foundation for the design of programming environments where programs are developed consistently with formal specifications.
    url: https://pauillac.inria.fr/~huet/PUBLIC/typtyp.pdf
    tags: 
      - Theory and Implementation of Rocq

  - author:
    - family: Coquand
      given: Thierry
    year: 1985
    publisher: PhD Thesis, Université Paris 7
    title: Une théorie des constructions
    abstract: >
      On propose une synthèse de différents systèmes de types: la théorie des types de Martin-Löf, le calcul d'ordre supérieur de Girard, et le calcul automath de De Bruijn. Le résultat fondamental de ce travail est une preuve de cohérence du calcul ainsi obtenu (la théorie des constructions). D'après les résultats de Girard, ce système a la puissance d'expression de l'arithmétique d'ordre supérieure. Les exemples développes sont de deux ordres: en logique (on retrouve les différents systèmes logiques connus) et en informatique (le type étant alors la spécification du programme)
    url: https://theses.fr/1985PA07F126
    tags: 
      - Theory and Implementation of Rocq