THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES

DOI10.1142/S0129054198000210zbMath1320.03036MaRDI QIDQ5248982

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

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

Cites Work

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

This page was built for publication: THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES