The soundness of explicit substitution with nameless variables

DOI10.1142/S0129054198000210MaRDI QIDQ5248982zbMATH OpenFDO

Authors Fairouz Kamareddine

Publication date 29 April 2015

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

zbMATH Keywords

soundnessexplicit substitutionde Bruijn indicesvariable names

Mathematics Subject Classification ID

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

Recommendations

• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• On explicit substitution with names
• On explicit substitutions and names (extended abstract)
• Explicit substitutions
• A \(\lambda\)-calculus with explicit weakening and explicit substitution

Cites work

• A unified approach to type theory through a refined -calculus
• A useful \(\lambda\)-notation
• Canonical typing and ∏-conversion in the Barendregt Cube
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• ON STEPWISE EXPLICIT SUBSTITUTION
• Refining reduction in the lambda calculus
• The categorical abstract machine

Cited in

(6)

• On explicit substitutions and names (extended abstract)
• Lazy variable-renumbering makes substitution cheap
• On explicit substitution with names
• A proof of the substitution lemma in de Bruijn's notation
• scientific article; zbMATH DE number 4120148 (Why is no real title available?)
• Computational soundness of a call by name calculus of recursively-scoped records

This page was built for publication: The soundness of explicit substitution with nameless variables

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