Inductively defined types in the Calculus of Constructions
- 1 January 1990
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 209-228
- https://doi.org/10.1007/bfb0040259
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Extracting ω's programs from proofs in the calculus of constructionsPublished by Association for Computing Machinery (ACM) ,1989
- The calculus of constructionsInformation and Computation, 1988
- Automatic synthesis of typed Λ-programs on term algebrasTheoretical Computer Science, 1985
- Constructions: A higher order proof system for mechanizing mathematicsLecture Notes in Computer Science, 1985
- Reasoning about functional programs and complexity classes associated with type disciplinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1983
- The Expressiveness of Simple and Second-Order Type StructuresJournal of the ACM, 1983
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972
- Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des TypesPublished by Elsevier BV ,1971