Higher order unification via explicit substitutions

DOI10.1006/inco.1999.2837zbMath1005.03016OpenAlexW2132119724MaRDI QIDQ1854337

Claude Kirchner, Gilles Dowek, Thérèse Hardin

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/5a62b1bc0db2794285fd18936e497e59b4e12648

zbMATH Keywords

lambda calculushigher-order unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items

Rewriting logic: Roadmap and bibliography, Nominal unification, Unnamed Item, Simplifying the signature in second-order unification, Unification for $$\lambda $$ -calculi Without Propagation Rules, Nominal essential intersection types, Choices in representation and reduction strategies for lambda terms in intensional contexts, Resource operators for \(\lambda\)-calculus, A \(\rho\)-calculus of explicit constraint application, Unnamed Item, Twenty years of rewriting logic, Formal categorical reasoning, Nominal techniques in Isabelle/HOL, Theorem proving modulo, Completeness in PVS of a nominal unification algorithm, The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations, Comparing Calculi of Explicit Substitutions with Eta-reduction, Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions, Comparing and implementing calculi of explicit substitutions with eta-reduction, A typed context calculus, Proof-term synthesis on dependent-type systems via explicit substitutions, Restricted combinatory unification, SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★, Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions, Equational rules for rewriting logic

Uses Software

• ETPS
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A combinatory logic approach to higher-order E-unification
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The undecidability of the second-order unification problem
• Simulation of Turing machines by a regular rewrite rule
• Unification under a mixed prefix
• Instantiation theory. On the foundations of automated deduction
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Completeness results for basic narrowing
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification via combinators
• An Efficient Unification Algorithm
• A Complete Proof Synthesis Method for the Cube of Type Systems
• Confluence properties of weak and strong calculi of explicit substitutions
• Dynamically-typed computations for order-sorted equational presentations
• Explicit substitutions
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Resolution in type theory
• The undecidability of unification in third order logic
• On finite representations of infinite sequences of terms
• Meta-rule synthesis from crossed rewrite systems