Explicit Substitutions à la de Bruijn

DOI10.1016/S1571-0661(04)80759-XzbMath1264.03044MaRDI QIDQ4924548

Fairouz Kamareddine, Alejandro Ríos

Publication date: 6 June 2013

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ On explicit substitutions and names (extended abstract) ⋮ A prismoid framework for languages with resources ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of term rewriting: Interpretation and type elimination
• A useful \(\lambda\)-notation
• Proof of termination of the rewriting system SUBSET on CCL
• Strong normalization of substitutions
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• ON STEPWISE EXPLICIT SUBSTITUTION
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Relating the   - and  s-styles of explicit substitutions
• Explicit substitutions

This page was built for publication: Explicit Substitutions à la de Bruijn