A compact kernel for the calculus of inductive constructions

DOI10.1007/s12046-009-0003-3zbMath1196.68221MaRDI QIDQ1040007

Claudio Sacerdoti Coen, Andrea Asperti, Wilmer Ricciotti, Enrico Tassi

Publication date: 23 November 2009

Published in: Sādhanā (Search for Journal in Brave)

Full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0071-0144

zbMATH Keywords

kernel; Matita; interactive theorem provers; calculus of inductive constructions

Mathematics Subject Classification ID

Related Items

Mtac: A monad for typed tactic programming in Coq, Formal metatheory of programming languages in the Matita interactive theorem prover, Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface, Formalising Overlap Algebras in Matita

Uses Software

• Coq
• OCaml
• Automath
• LEGO

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Inductive families
• Strongly reducing variants of the Krivine abstract machine
• Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I
• Crafting a Proof Assistant
• About the Formalization of Some Results by Chebyshev in Number Theory
• Termination checking with types
• A categorical understanding of environment machines
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Mathematical Knowledge Management
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item