Pattern matching as cut elimination

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

zbMATH Keywords

typed pattern calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

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

• ML
• Haskell
• Miranda
• MiniML

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