Explicit substitutions à la de Bruijn: the local and global way

DOI10.1016/S1571-0661(04)80759-XMaRDI QIDQ4924548zbMATH OpenFDO

Authors Fairouz Kamareddine, A. Ríos

Publication date 6 June 2013

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

Full work available at URL https://doi.org/10.1016/S1571-0661(04)80759-X

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1342288
• Comparing calculi of explicit substitutions with eta-reduction
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Confluence properties of weak and strong calculi of explicit substitutions
• Explicit substitutions

Cites work

• A useful -notation
• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• scientific article; zbMATH DE number 4048997 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 794240 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• ON STEPWISE EXPLICIT SUBSTITUTION
• Proof of termination of the rewriting system SUBSET on CCL
• Relating the   - and  s-styles of explicit substitutions
• Strong normalization of substitutions
• Termination of term rewriting: Interpretation and type elimination
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(7)

• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• On explicit substitutions and names (extended abstract)
• Comparing calculi of explicit substitutions with eta-reduction
• scientific article; zbMATH DE number 1424036 (Why is no real title available?)
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• A prismoid framework for languages with resources

This page was built for publication: Explicit substitutions à la de Bruijn: the local and global way

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