A compact kernel for the calculus of inductive constructions
type: Item
instance of: scholarly article
title: A compact kernel for the calculus of inductive constructions
zbMATH Open document ID: 1196.68221
published in: Sādhanā
publication date: 2009-11-23T00:00:00Z
full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0071-0144
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5637281
zbMATH Keywords: interactive theorem provers
zbMATH Keywords: calculus of inductive constructions
zbMATH Keywords: Matita
zbMATH Keywords: kernel
author: Andrea Asperti
author: Wilmer Ricciotti
author: Claudio Sacerdoti Coen
author: Enrico Tassi
describes a project that uses: OCaml
describes a project that uses: Coq
describes a project that uses: Automath
describes a project that uses: LEGO
MaRDI profile type: Publication
OpenAlex ID: W2038098277
cites work: Termination checking with types
cites work: A categorical understanding of environment machines
cites work: About the Formalization of Some Results by Chebyshev in Number Theory
cites work: Crafting a Proof Assistant
cites work: Theoretical Pearls:Representing ‘undefined’ in lambda calculus
cites work: CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q4484336
cites work: Strongly reducing variants of the Krivine abstract machine
cites work: Inductive families
cites work: Q4411846
cites work: Q3685171
cites work: Q4435473
cites work: Q4692880
cites work: Mathematical Knowledge Management
cites work: Reduction and conversion strategies for the calculus of (co)inductive constructions. I
cites work: Q4364399
DOI: 10.1007/S12046-009-0003-3
description: scientific article; zbMATH DE number 5637281