Explicit Substitutions à la de Bruijn
From MaRDI portal
Publication:4924548
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)
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