Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
From MaRDI portal
Publication:1575247
DOI10.1016/S0304-3975(98)00166-2zbMath0944.68033MaRDI QIDQ1575247
Publication date: 21 August 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items (7)
Pattern matching as cut elimination ⋮ On explicit substitution with names ⋮ Pure type systems with explicit substitutions ⋮ Compositional Z: confluence proofs for permutative conversion ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
Cites Work
- The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
- Combinatory reduction systems: Introduction and survey
- Termination of term rewriting: Interpretation and type elimination
- Eta-conversion for the languages of explicit substitutions
- Combining algebraic rewriting, extensional lambda calculi, and fixpoints
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- Proof of termination of the rewriting system SUBSET on CCL
- Higher order unification via explicit substitutions
- Functional back-ends within the lambda-sigma calculus
- λ-calculi with explicit substitutions and composition which preserve β-strong normalization
- λν, a calculus of explicit substitutions which preserves strong normalisation
- A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
- The virtues of eta-expansion
- Explicit substitutions
- Some lambda calculi with categorical sums and products
- Combinatory reduction systems with explicit substitution that preserve strong normalisation
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
