A unification algorithm for typed \(\overline\lambda\)-calculus

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

Mathematics Subject Classification ID

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, Synthesis of rewrite programs by higher-order and semantic unification, Expressing combinatory reduction systems derivations in the rewriting calculus, Choices in representation and reduction strategies for lambda terms in intensional contexts, On connections and higher-order logic, A characterization of lambda definable tree operations, Conditional equational theories and complete sets of transformations, The calculus of context relations, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, Word operation definable in the typed \(\lambda\)-calculus, Delaying unification algorithms for lambda calculi, A practically efficient and almost linear unification algorithm, The calculus of constructions, A unification algorithm for second-order monadic terms, 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, Mechanizing \(\omega\)-order type theory through unification, The typed lambda-calculus is not elementary recursive, 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, Complete sets of unifiers and matchers in equational theories, The foundation of a generic theorem prover, On the logic of unification, Higher-order unification revisited: Complete sets of transformations, The linked conjunct method for automatic deduction and related search techniques, 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, Automation for interactive proof: first prototype, Decidability of bounded higher-order unification, Uniform proofs as a foundation for logic programming, Tractable and intractable second-order matching problems

Cites Work