Constructions: A higher order proof system for mechanizing mathematics
- 1 January 1985
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 151-184
- https://doi.org/10.1007/3-540-15983-5_13
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Polymorphism is not set-theoreticLecture Notes in Computer Science, 1984
- Automating Higher-Order LogicContemporary Mathematics, 1984
- The Expressiveness of Simple and Second-Order Type StructuresJournal of the ACM, 1983
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- A Complete Mechanization of Second-Order Type TheoryJournal of the ACM, 1973
- A complete mechanization of (ω) -order type theoryPublished by Association for Computing Machinery (ACM) ,1972
- Resolution in type theoryThe Journal of Symbolic Logic, 1971
- 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
- Constructive validityPublished by Springer Science and Business Media LLC ,1970
- On Theories with a Combinatorial Definition of "Equivalence"Annals of Mathematics, 1942