Mechanizing \(\omega\)-order type theory through unification
From MaRDI portal
Publication:1239309
DOI10.1016/0304-3975(76)90021-9zbMath0361.02020MaRDI QIDQ1239309
D. C. Jensen, Tomasz Pietrzykowski
Publication date: 1977
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(76)90021-9
Related Items
Unification under a mixed prefix, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, A higher-order unification algorithm for inductive types and dependent types, Higher-order unification via combinators
Cites Work
- A unification algorithm for typed \(\overline\lambda\)-calculus
- A Machine-Oriented Logic Based on the Resolution Principle
- Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
- Resolution in type theory
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- Completeness in the theory of types
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item