ISSN:
1433-299X
Schlagwort(e):
Typed lambda calculus
;
Higher order logic
;
Strong normalisation theorem
;
Consistency of assumptions
Quelle:
Springer Online Journal Archives 1860-2000
Thema:
Informatik
Notizen:
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.
Materialart:
Digitale Medien
URL:
http://dx.doi.org/10.1007/BF01211392
Permalink