The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations

DOI10.1016/S1571-0661(04)80539-5zbMath1261.68043MaRDI QIDQ4916200

Gopalan Nadathur

Publication date: 19 April 2013

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

zbMATH Keywords

logical frameworkexplicit substitutionsuspension notation

Mathematics Subject Classification ID

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

Related Items

A \(\rho\)-calculus of explicit constraint application ⋮ Lambda-calculus with director strings ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction

Uses Software

• Teyjus

Cites Work

• A notation for lambda terms. A generalization of environments
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Higher order unification via explicit substitutions
• A λ-calculus with explicit weakening and explicit substitution
• λν, a calculus of explicit substitutions which preserves strong normalisation
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• The λs_e-calculus does not preserve strong normalisation
• Explicit substitutions
• Unnamed Item
• Unnamed Item
• Unnamed Item