 |
 |
 |
 |
Conference papers
Intuitionistic Sequent-Style Calculus with Explicit Structural Rules
Abstract : In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit weakening and contraction. We study a system derived from /\-Gtz of Espirito Santo by adding explicit operators for weakening and contraction, which we call l/\-Gtz. This system contains only linear terms. For the proposed calculus we introduce the type assignment system with simple types. The presented system has a natural diagrammatic representation, which is used for proving the subject reduction property. We prove the strong normalisation property by embedding l/\-Gtz into the simply typed /\lxr calculus of Kesner and Lengrand.
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00654762
Contributor : Pierre Lescanne Connect in order to contact the contributor
Submitted on : Thursday, December 22, 2011 - 8:52:28 PM
Last modification on : Saturday, September 11, 2021 - 3:17:03 AM
Contributor : Pierre Lescanne Connect in order to contact the contributor
Submitted on : Thursday, December 22, 2011 - 8:52:28 PM
Last modification on : Saturday, September 11, 2021 - 3:17:03 AM