Comparing and implementing calculi of explicit substitutions with eta-reduction

DOI10.1016/J.APAL.2004.06.009MaRDI QIDQ1779307zbMATH OpenOpenAlexDBLPWikidataFDO

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

Publication date 1 June 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2004.06.009

zbMATH Keywords

\(\lambda\)-calculieta-reductionexplicit substitutionssuspension calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Recommendations

• Comparing 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
• scientific article; zbMATH DE number 2185655
• Relating the   - and  s-styles of explicit substitutions

Cites work

• -calculi with explicit substitutions and composition which preserve -strong normalization
• A notation for lambda terms. A generalization of environments
• A useful -notation
• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• Combinatory reduction systems with explicit substitution that preserve strong normalisation
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Confluence properties of weak and strong calculi of explicit substitutions
• Cut rules and explicit substitutions
• Explicit substitutions
• Explicit substitutions with de bruijn's levels
• Explicit substitutions à la de Bruijn: the local and global way
• 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 2185655 (Why is no real title available?)
• scientific article; zbMATH DE number 1300968 (Why is no real title available?)
• 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 2090073 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 2208065 (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 suspension notation for lambda terms and its use in metalanguage implementations
• 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

(7)

• Eta-conversion for the languages of explicit substitutions
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• scientific article; zbMATH DE number 2185655 (Why is no real title available?)
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
• Explicit substitutions calculi with one step eta-reduction decided explicitly
• Comparing calculi of explicit substitutions with eta-reduction
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi

Describes a project that uses

Uses Software

• Automath
• ALF

This page was built for publication: Comparing and implementing 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 Q1779307)