Intuitionistic Sequent-Style Calculus with Explicit Structural Rules

Pierre Lescanne 1 Silvia Ghilezan 2 Jelena Ivetic 2 Dragisa Zunic
1 LIP - Laboratoire de l'Informatique du Parallélisme
2 Faculty of engineering, University of Novi Sad
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.
Document type :
Conference papers
Complete list of metadatas
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00654762
Contributor : Pierre Lescanne <>
Submitted on : Thursday, December 22, 2011 - 8:52:28 PM
Last modification on : Wednesday, November 20, 2019 - 3:01:26 AM

Identifiers

  • HAL Id : ensl-00654762, version 1

Collections

ENS-LYON | CNRS | INRIA | LIP | INSMI | UNIV-LYON1 | UDL

Citation

Pierre Lescanne, Silvia Ghilezan, Jelena Ivetic, Dragisa Zunic. Intuitionistic Sequent-Style Calculus with Explicit Structural Rules. Logic, Language, and Computation - 8th International Tbilisi Symposium on Logic, Language, and Computation, Sep 2009, Bakuriani, Georgia. pp.101-124. ⟨ensl-00654762⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

153

Contact

Informations

CCSD