A unification algorithm for typed \(\bar\lambda\)-calculus
From MaRDI portal
Publication:1227601
DOI10.1016/0304-3975(75)90011-0zbMath0332.02035MaRDI QIDQ1227601
Publication date: 1975
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(75)90011-0
03B40: Combinatory logic and lambda calculus
Related Items
TPS: A hybrid automatic-interactive system for developing proofs, Finite generation of ambiguity in context-free languages, Theorem proving modulo, Middle-out reasoning for synthesis and induction, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, Automatic theorem proving. II, Unnamed Item, Decidability of the unification problem for second-order languages with unary functional symbols, Unnamed Item
Cites Work
- Mechanizing \(\omega\)-order type theory through unification
- Application à la viscoélasticité non linéaire du calcul symbolique à plusieurs variables
- A Machine-Oriented Logic Based on the Resolution Principle
- Resolution in type theory
- A Complete Mechanization of Second-Order Type Theory
- The undecidability of unification in third order logic
- A formulation of the simple theory of types
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item