Pattern matching as cut elimination

DOI10.1016/J.TCS.2004.03.032MaRDI QIDQ1882898zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A typed pattern calculus
• scientific article; zbMATH DE number 2090072
• Pure patterns type systems
• Functional and Logic Programming
• Cut rules and explicit substitutions

Cites work

• scientific article; zbMATH DE number 2185670 (Why is no real title available?)
• scientific article; zbMATH DE number 3951980 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• scientific article; zbMATH DE number 555217 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 1405629 (Why is no real title available?)
• A modal analysis of staged computation
• A typed pattern calculus
• Abstract data type systems
• Combinatory reduction systems with explicit substitution that preserve strong normalisation
• Computational interpretations of linear logic
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Cut rules and explicit substitutions
• Explicit substitutions
• Orderings for term-rewriting systems
• Pattern matching as cut elimination
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The rewriting calculus. I
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(7)

• scientific article; zbMATH DE number 2090072 (Why is no real title available?)
• Expression reduction systems with patterns
• Solvability = typability + inhabitation
• Pattern matching as cut elimination
• Pure patterns type systems
• Resource operators for \(\lambda\)-calculus
• Pure pattern calculus à la de Bruijn

Describes a project that uses

Uses Software

• MiniML
• Miranda
• Haskell
• ML

This page was built for publication: Pattern matching as cut elimination

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