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

explicit substitutions\(\lambda\)-calculieta-reductionsuspension calculus

Mathematics Subject Classification ID

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

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

• 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?)
• A notation for lambda terms. A generalization of environments
• A useful \(\lambda\)-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
• 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 \(\lambda s_e\)-style of explicit substitutions
• \(\lambda\)-calculi with explicit substitutions and composition which preserve \(\beta\)-strong normalization
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(7)

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

Describes a project that uses

Uses Software

• ALF
• Automath

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)