Comparing calculi of explicit substitutions with eta-reduction

DOI10.1016/S1571-0661(04)80542-5MaRDI QIDQ4916203zbMATH OpenOpenAlexWikidataFDO

Authors Mauricio Ayala-Rincón, Flávio L. C. de Moura, Fairouz Kamareddine

Publication date 19 April 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)80542-5

zbMATH Keywords

calculi of explicit substitutionseta reductionlambda-calculi

Mathematics Subject Classification ID

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

Recommendations

• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Explicit substitutions calculi with one step eta-reduction decided explicitly
• Eta-conversion for the languages of explicit substitutions
• Relating the   - and  s-styles of explicit substitutions
• Explicit substitutions à la de Bruijn: the local and global way

Cites work

• -calculi with explicit substitutions and composition which preserve -strong normalization
• A notation for lambda terms. A generalization of environments
• A useful -notation
• Confluence properties of weak and strong calculi of explicit substitutions
• Cut rules and explicit substitutions
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Functional runtime systems within the lambda-sigma calculus
• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 1332643 (Why is no real title available?)
• scientific article; zbMATH DE number 1332647 (Why is no real title available?)
• scientific article; zbMATH DE number 1070568 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• ON STEPWISE EXPLICIT SUBSTITUTION
• Relating the   - and  s-styles of explicit substitutions
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The λs_e-calculus does not preserve strong normalisation
• Unification via the s_e-style of explicit substitutions
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(12)

• Eta-conversion for the languages of explicit substitutions
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 2185655 (Why is no real title available?)
• Unification for -calculi without propagation rules
• A Theory of Explicit Substitutions with Safe and Full Composition
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
• Explicit substitutions calculi with one step eta-reduction decided explicitly
• Relating the   - and  s-styles of explicit substitutions
• The suspension notation for lambda terms and its use in metalanguage implementations
• Explicit substitutions à la de Bruijn: the local and global way
• On the computability of relations on -terms and Rice's theorem -- the case of the expansion problem for explicit substitutions
• Foundations of Software Science and Computational Structures

Describes a project that uses

Uses Software

• ALF
• Automath

This page was built for publication: Comparing calculi of explicit substitutions with eta-reduction

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