Unification for -calculi without propagation rules

DOI10.1007/978-3-319-46750-4_11MaRDI QIDQ3179400zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Recommendations

• Higher order unification via explicit substitutions
• Unification via the 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

Cites work

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

Cited in

(4)

• Delaying unification algorithms for lambda calculi
• Unification via the s_e-style of explicit substitutions
• scientific article; zbMATH DE number 1303341 (Why is no real title available?)
• scientific article; zbMATH DE number 3997190 (Why is no real title available?)

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)