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

03B35: Mechanization of proofs and logical operations

03B40: Combinatory logic and lambda calculus

Related Items

On explicit substitutions and names (extended abstract), Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (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