Name
Abstract | ||
|---|---|---|
We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for minimal logic. Our calculus is inspired by the Curry-Howard Isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequent proof normalization performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w.r.t a system with meta-level substitutions and strong normalization for well-typed terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with meta-level operations for pattern matching and substitutions. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1016/j.tcs.2004.03.032 | Theoretical Computer Science |
Keywords | DocType | Volume |
gentzen sequent calculus,strong normalization w,pattern matching,sequent proof normalization step,explicit substitutions,implementation calculus,cut elimination,subject reduction,pattern calculus,proof normalization,-calculi,reduction rule,explicit pattern matching,strong normalization,encoding,functional programming,calculus,computational modeling,sequent calculus,confluence,embedded computing,minimal logic,type theory,theorem proving,network address translation,curry howard isomorphism,logic | Journal | 323 |
Issue | ISSN | ISBN |
1 | Theoretical Computer Science | 0-7695-0158-3 |
Citations | PageRank | References |
9 | 0.72 | 20 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Serenella Cerrito | 1 | 139 | 13.72 |
| Delia Kesner | 2 | 369 | 39.75 |