A unification algorithm for typed \(\overline\lambda\)-calculus
From MaRDI portal
Publication:1230505
DOI10.1016/0304-3975(75)90011-0zbMath0337.68027MaRDI QIDQ1230505
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
68Q25: Analysis of algorithms and problem complexity
68W30: Symbolic computation and algebraic computation
03B40: Combinatory logic and lambda calculus
68W99: Algorithms in computer science
Related Items
Proof-term synthesis on dependent-type systems via explicit substitutions, A combinatory logic approach to higher-order E-unification, A notation for lambda terms. A generalization of environments, Polymorphic rewriting conserves algebraic strong normalization, Horn clause programs with polymorphic types: Semantics and resolution, Natural language syntax and first-order inference, Unification under a mixed prefix, A relaxation approach to splitting in an automatic theorem prover, A unification algorithm for typed \(\overline\lambda\)-calculus, Unification with extended patterns, A decision algorithm for distributive unification, Unification problem in equational theories, Decidability of behavioural equivalence in unary PCF, Implementing tactics and tacticals in a higher-order logic programming language, A proof procedure for the logic of hereditary Harrop formulas, Set theory for verification. I: From foundations to functions, Third order matching is decidable, Reduction and unification in lambda calculi with a general notion of subtype, A semantics for \(\lambda \)Prolog, The Qu-Prolog unification algorithm: formalisation and correctness, A higher-order unification algorithm for inductive types and dependent types, Unification of infinite sets of terms schematized by primal grammars, Encoding transition systems in sequent calculus, Cut-elimination for a logic with definitions and induction, Proof-search in type-theoretic languages: An introduction, Program development schemata as derived rules, Higher order unification via explicit substitutions, Decidability of bounded second order unification, Normal forms in combinatory logic, TPS: A theorem-proving system for classical type theory, Proving theorems by reuse, Higher-order unification via combinators
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Mechanizing \(\omega\)-order type theory through unification
- 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
