Name
Abstract | ||
|---|---|---|
We investigate some syntactic properties of Wadler’s dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot’s λμ calculus corresponds to classical natural deduction. Our main result is strong normalization theorem for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11591191_13 | LPAR |
Keywords | Field | DocType |
classical logic,natural deduction,sequent calculus,functional programming,programming paradigm | Discrete mathematics,Typed lambda calculus,Simply typed lambda calculus,Natural deduction,Proof calculus,Algorithm,Noncommutative logic,Sequent,Cut-elimination theorem,Mathematics,Curry–Howard correspondence | Conference |
Volume | ISSN | ISBN |
3835 | 0302-9743 | 3-540-30553-X |
Citations | PageRank | References |
7 | 0.66 | 24 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel J. Dougherty | 1 | 413 | 32.13 |
| Silvia Ghilezan | 2 | 106 | 14.66 |
| Pierre Lescanne | 3 | 925 | 123.70 |
| Silvia Likavec | 4 | 116 | 15.35 |