ISSN:
1433-299X
Keywords:
Typed lambda calculus
;
Higher order logic
;
Strong normalisation theorem
;
Consistency of assumptions
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract The calculus of constructions of Coquand, which is a version of higher order typedλ-calculus based on the dependent function type, is considered from the perspective of its use as the mathematical foundation for a proof development system. The paper considers formulations of the calculus, the underlying consistency of the formalism (i.e., the strong normalisation theorem), and the proof theory of adding assumptions for notions from logic and set theory. Proofs are not given, but references to them are.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01211392
Permalink