Strong Normalization of the Dual Classical Sequent Calculus

13 years 10 months ago

Download web.cs.wpi.edu

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 conﬂuence results for the typed and untyped versions of the system.

Daniel J. Dougherty, Silvia Ghilezan, Pierre Lesca

Real-time Traffic

Dual Calculus | LPAR 2005 | Parigot’s λµ Calculus | Wadler’s Dual Calculus |

claim paper

» An Isomorphism Between CutElimination Procedure and Proof Reduction

» Classical BI Its Semantics and Proof Theory

» Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi

» Principles of Superdeduction

» Strong normalization of a symmetric lambda calculus for secondorder classical logic

» Strong Normalization of Classical Natural Deduction with Disjunction

» Kripke models for classical logic

» Strong normalization from an unusual point of view

Post Info
More Details (n/a)

Added	28 Jun 2010
Updated	28 Jun 2010
Type	Conference
Year	2005
Where	LPAR
Authors	Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec

Comments (0)

Sciweavers

Strong Normalization of the Dual Classical Sequent Calculus

Dual Calculus | LPAR 2005 | Parigot’s λµ Calculus | Wadler’s Dual Calculus |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers