Authors: Ghilezan, Silvia 
Ivetić, Jelena
Lescanne, Pierre
Žunić, Dragiša
Title: Intuitionistic sequent-style calculus with explicit structural rules
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume: 6618 LNAI
First page: 101
Last page: 124
Conference: 8th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2009; Bakuriani; Georgia; 21 September 2009 through 25 September 2009
Issue Date: 1-Aug-2011
Rank: M33
ISBN: 978-3-642-22302-0
ISSN: 0302-9743
DOI: 10.1007/978-3-642-22303-7_7
In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit structural rules of weakening and contraction. We present a linear term calculus derived from the calculus of Espírito Santo, which captures the computational content of the intuitionistic sequent logic, by adding explicit operators for weakening and contraction. For the proposed calculus we introduce the type assignment system with simple types and prove some operational properties, including the subject reduction and strong normalisation property. We then relate the proposed linear type calculus to the simply typed intuitionistic calculus of Kesner and Lengrand, which handles explicit operators of weakening and contraction in the natural deduction framework.
Publisher: Springer Link

Show full item record


checked on Jun 23, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.