Please use this identifier to cite or link to this item:
https://open.uns.ac.rs/handle/123456789/13655
Title: | Intuitionistic sequent-style calculus with explicit structural rules | Authors: | Gilezan, Silvia Ivetić, Jelena Lescanne P. Žunić, D. |
Issue Date: | 1-Aug-2011 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | 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. © 2011 Springer-Verlag. | URI: | https://open.uns.ac.rs/handle/123456789/13655 | ISBN: | 9783642223020 | ISSN: | 3029743 | DOI: | 10.1007/978-3-642-22303-7_7 |
Appears in Collections: | FTN Publikacije/Publications |
Show full item record
SCOPUSTM
Citations
1
checked on Aug 26, 2023
Page view(s)
47
Last Week
16
16
Last month
0
0
checked on May 3, 2024
Google ScholarTM
Check
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.