Inductively defined types in the Calculus of Constructions

This publication has 8 references indexed in Scilit:

• Extracting ω's programs from proofs in the calculus of constructions
  Published by Association for Computing Machinery (ACM) ,1989
• The calculus of constructions
  Information and Computation, 1988
• Automatic synthesis of typed Λ-programs on term algebras
  Theoretical Computer Science, 1985
• Constructions: A higher order proof system for mechanizing mathematics
  Published by Springer Nature ,1985
• Reasoning about functional programs and complexity classes associated with type disciplines
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,1983
• The Expressiveness of Simple and Second-Order Type Structures
  Journal of the ACM, 1983
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem
  Indagationes Mathematicae, 1972
• Une Extension De ĽInterpretation De Gödel a ĽAnalyse, Et Son Application a ĽElimination Des Coupures Dans ĽAnalyse Et La Theorie Des Types
  Published by Elsevier ,1971