Coquand's calculus of constructions: A mathematical foundation for a proof development system
type: Item
instance of: scholarly article
title: Coquand's calculus of constructions: A mathematical foundation for a proof development system
zbMATH Open document ID: 0766.03007
DOI: 10.1007/BF01211392
author: Jonathan P. Seldin
published in: Formal Aspects of Computing
publication date: 1993-01-17T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 68N15
Mathematics Subject Classification ID: 68Q99
zbMATH DE Number: 97536
zbMATH Keywords: consistency of assumptions
zbMATH Keywords: calculus of constructions
zbMATH Keywords: higher order typed \(\lambda\)-calculus
zbMATH Keywords: proof development system
zbMATH Keywords: normalisation
describes a project that uses: Nuprl
MaRDI profile type: Publication
cites work: A transfinite type theory with type variables
cites work: The calculus of constructions
cites work: Q5547552
cites work: Combinatory logic. With two sections by William Craig.
cites work: Combinatory logic. Vol. II
cites work: Q3856127
cites work: Q5667469
cites work: Q5815602
cites work: Q4722037
cites work: Q3211296
cites work: Q4099613
cites work: Q5559220
cites work: A sequent calculus for type assignment
cites work: On the proof theory of Coquand's calculus of constructions
full work available at URL: https://doi.org/10.1007/bf01211392
OpenAlex ID: W2012195956
description: scientific article; zbMATH DE number 97536