Unification for -calculi without propagation rules

DOI10.1007/978-3-319-46750-4_11zbMATH Open1482.68080OpenAlexW2522173973MaRDI QIDQ3179400FDOQ3179400

Authors: 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

Recommendations

• Higher order unification via explicit substitutions
• Unification via the \(\lambda s_e\)-style of explicit substitutions
• scientific article; zbMATH DE number 1088023
• Comparing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 1303341

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Delaying unification algorithms for lambda calculi
• Title not available (Why is that?)
• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Title not available (Why is that?)

This page was built for publication: Unification for \(\lambda\)-calculi without propagation rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179400)