Introduction to the Calculus of Inductive Constructions
| Autor: | Paulin-Mohring, Christine |
|---|---|
| Přispěvatelé: | Paulin-Mohring, Christine, Bruno Woltzenlogel Paleo, David Delahaye, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Coq proof assistant
Calculus of Inductive Constructions TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Computer Science::Programming Languages ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.2: Logics of programs ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs |
| Zdroj: | All about Proofs, Proofs for All Bruno Woltzenlogel Paleo; David Delahaye. All about Proofs, Proofs for All, 55, College Publications, 2015, Studies in Logic (Mathematical logic and foundations), 978-1-84890-166-7 |
| Popis: | International audience; This paper gives an introduction to the Calculus of Inductive Constructions, the formalism behind the Coq proof assistant. We present the language and the typing rules, starting with the pure functional part and then introducing the inductive declarations. We briefly discuss the properties of this language, both from the theoretical and pragmatic points of view and give examples of applications. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|