Encoding a dependent-type λ-calculus in a logic programming language
Authors:
- 1 January 1990
- book chapter
- Published by Springer Nature
- p. 221-235
Abstract
No abstract availableKeywords
This publication has 4 references indexed in Scilit:
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- The calculus of constructionsInformation and Computation, 1988
- Ideas and Results in Proof Theory1971
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940