A compact kernel for the calculus of inductive constructions
From MaRDI portal
Publication:1040007
DOI10.1007/s12046-009-0003-3zbMath1196.68221MaRDI QIDQ1040007
Enrico Tassi, Andrea Asperti, Claudio Sacerdoti Coen, Wilmer Ricciotti
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
Related Items
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
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