A compact kernel for the calculus of inductive constructions

DOI10.1007/S12046-009-0003-3MaRDI QIDQ1040007zbMATH OpenOpenAlexFDO

Authors Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, 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

kernelMatitainteractive theorem proverscalculus of inductive constructions

Mathematics Subject Classification ID

Recommendations

• The Matita interactive theorem prover
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A Short Presentation of Coq
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• scientific article; zbMATH DE number 1301729

Cites work

• scientific article; zbMATH DE number 3907750 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 1948185 (Why is no real title available?)
• scientific article; zbMATH DE number 2003160 (Why is no real title available?)
• scientific article; zbMATH DE number 1927418 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• A categorical understanding of environment machines
• About the Formalization of Some Results by Chebyshev in Number Theory
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Crafting a Proof Assistant
• Inductive families
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mathematical Knowledge Management
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• Strongly reducing variants of the Krivine abstract machine
• Termination checking with types
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus

Cited in

(7)

• Asynchronous processing of Coq documents: from the kernel up to the user interface
• Formalising overlap algebras in Matita
• Formal metatheory of programming languages in the Matita interactive theorem prover
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• Mtac: a monad for typed tactic programming in Coq
• Building Decision Procedures in the Calculus of Inductive Constructions
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I

Describes a project that uses

Uses Software

• Coq
• OCaml
• Automath
• LEGO

This page was built for publication: A compact kernel for the calculus of inductive constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1040007)