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

DOI10.1016/0304-3975(75)90011-0zbMath0337.68027OpenAlexW2034676877MaRDI 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

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Combinatory logic and lambda calculus (03B40) Algorithms in computer science (68W99)

Related Items (79)

Higher-order unification via combinators ⋮ Third order matching is decidable ⋮ Linear unification of higher-order patterns ⋮ Reduction and unification in lambda calculi with a general notion of subtype ⋮ Decidability of bounded second order unification ⋮ Simplifying the signature in second-order unification ⋮ A termination ordering for higher order rewrite systems ⋮ A restricted form of higher-order rewriting applied to an HDL semantics ⋮ Efficient second-order matching ⋮ Linear second-order unification ⋮ Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type ⋮ A semantics for \(\lambda \)Prolog ⋮ The Qu-Prolog unification algorithm: formalisation and correctness ⋮ Word operation definable in the typed \(\lambda\)-calculus ⋮ Nominal essential intersection types ⋮ Uniform proofs as a foundation for logic programming ⋮ Delaying unification algorithms for lambda calculi ⋮ A practically efficient and almost linear unification algorithm ⋮ Normal forms in combinatory logic ⋮ Tractable and intractable second-order matching problems ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ A higher-order unification algorithm for inductive types and dependent types ⋮ The calculus of constructions ⋮ A unification algorithm for second-order monadic terms ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ TPS: A theorem-proving system for classical type theory ⋮ A notation for lambda terms. A generalization of environments ⋮ From programming-by-example to proving-by-example ⋮ Modular AC unification of higher-order patterns ⋮ Higher order disunification: Some decidable cases ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ Nominal abstraction ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ The Alf proof editor and its proof engine ⋮ Semantics for abstract clauses ⋮ Encoding transition systems in sequent calculus ⋮ Automation for interactive proof: first prototype ⋮ 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 ⋮ Polymorphic rewriting conserves algebraic strong normalization ⋮ Horn clause programs with polymorphic types: Semantics and resolution ⋮ Decidability of bounded higher-order unification ⋮ Proving theorems by reuse ⋮ A combinatory logic approach to higher-order E-unification ⋮ Natural language syntax and first-order inference ⋮ Unification under a mixed prefix ⋮ A relaxation approach to splitting in an automatic theorem prover ⋮ Focused Inductive Theorem Proving ⋮ A unification algorithm for typed \(\overline\lambda\)-calculus ⋮ Mechanizing \(\omega\)-order type theory through unification ⋮ From LCF to Isabelle/HOL ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions ⋮ Making higher-order superposition work ⋮ Unification in an extensional lambda calculus with ordered function sorts and constant overloading ⋮ Decidable higher-order unification problems ⋮ Theory and practice of minimal modular higher-order E-unification ⋮ The typed lambda-calculus is not elementary recursive ⋮ Synthesis of rewrite programs by higher-order and semantic unification ⋮ Unification with extended patterns ⋮ A decision algorithm for distributive unification ⋮ 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 ⋮ Unification problem in equational theories ⋮ On equality up-to constraints over finite trees, context unification, and one-step rewriting ⋮ Partial matching for analogy discovery in proofs and counter-examples ⋮ Decidability of behavioural equivalence in unary PCF ⋮ Cut-elimination for a logic with definitions and induction ⋮ Proof-search in type-theoretic languages: An introduction ⋮ The linked conjunct method for automatic deduction and related search techniques ⋮ Program development schemata as derived rules ⋮ Higher order unification via explicit substitutions ⋮ 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 ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Cites Work

This page was built for publication: A unification algorithm for typed \(\overline\lambda\)-calculus