The suspension notation for lambda terms and its use in metalanguage implementations

DOI10.1016/S1571-0661(04)80539-5MaRDI QIDQ4916200zbMATH OpenFDO

Authors Gopalan Nadathur

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)80539-5

zbMATH Keywords

explicit substitutionlogical frameworksuspension notation

Mathematics Subject Classification ID

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

Recommendations

• A notation for lambda terms. A generalization of environments
• scientific article; zbMATH DE number 1332647
• Comparing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 2090073
• Higher-order substitutions

Cites work

• A -calculus with explicit weakening and explicit substitution
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A notation for lambda terms. A generalization of environments
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Higher order unification via explicit substitutions
• scientific article; zbMATH DE number 2185670 (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?)
• The λs_e-calculus does not preserve strong normalisation
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(4)

• Lambda-calculus with director strings
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 2090073 (Why is no real title available?)
• A \(\rho\)-calculus of explicit constraint application

Describes a project that uses

Uses Software

• Teyjus

This page was built for publication: The suspension notation for lambda terms and its use in metalanguage implementations

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