Pattern matching as cut elimination
From MaRDI portal
Publication:1882898
DOI10.1016/j.tcs.2004.03.032zbMath1078.68135OpenAlexW2021119395MaRDI QIDQ1882898
Serenella Cerrito, Delia Kesner
Publication date: 1 October 2004
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2004.03.032
Related Items (5)
Pattern matching as cut elimination ⋮ Resource operators for \(\lambda\)-calculus ⋮ Unnamed Item ⋮ Pure pattern calculus à la de Bruijn ⋮ Expression reduction systems with patterns
Uses Software
Cites Work
- Orderings for term-rewriting systems
- Computational interpretations of linear logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
- Abstract data type systems
- Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
- Pattern matching as cut elimination
- A typed pattern calculus
- Cut rules and explicit substitutions
- The rewriting calculus - part I
- λν, a calculus of explicit substitutions which preserves strong normalisation
- A modal analysis of staged computation
- Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
- Explicit substitutions
- 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
This page was built for publication: Pattern matching as cut elimination