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 (25)

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

This page was built for publication: Higher order unification via explicit substitutions