Unification for $$\lambda $$ -calculi Without Propagation Rules

DOI10.1007/978-3-319-46750-4_11zbMath1482.68080OpenAlexW2522173973MaRDI QIDQ3179400

Flávio L. C. de Moura

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-46750-4_11

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Third order matching is decidable
• Higher-order unification revisited: Complete sets of transformations
• Higher order unification via explicit substitutions
• Higher-order unification via combinators
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• Unification via the  se-style of explicit substitutions
• Distilling abstract machines
• Local Bigraphs and Confluence: Two Conjectures
• Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
• The Permutative λ-Calculus
• λν, a calculus of explicit substitutions which preserves strong normalisation
• A Theory of Explicit Substitutions with Safe and Full Composition
• The Structural λ-Calculus
• A Game-Theoretic Approach to Deciding Higher-Order Matching
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Decidability of fourth-order matching
• The λs_e-calculus does not preserve strong normalisation
• Higher Order   Matching is Undecidable
• Explicit substitutions
• A nonstandard standardization theorem
• The undecidability of unification in third order logic
• Logic for Programming, Artificial Intelligence, and Reasoning