The soundness of explicit substitution with nameless variables

DOI10.1142/S0129054198000210zbMATH Open1320.03036MaRDI QIDQ5248982FDOQ5248982

Authors: Fairouz Kamareddine 

Publication date: 29 April 2015

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

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

zbMATH Keywords

soundnessexplicit substitutionde Bruijn indicesvariable names

Mathematics Subject Classification ID

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

Cites Work

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

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
• Title not available (Why is that?)
• 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)