Молимо вас користите овај идентификатор за цитирање или овај линк до ове ставке:
https://open.uns.ac.rs/handle/123456789/13655
Назив: | Intuitionistic sequent-style calculus with explicit structural rules | Аутори: | Gilezan, Silvia Ivetić, Jelena Lescanne P. Žunić, D. |
Датум издавања: | 1-авг-2011 | Часопис: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Сажетак: | 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 |
Налази се у колекцијама: | FTN Publikacije/Publications |
Приказати целокупан запис ставки
SCOPUSTM
Навођења
1
проверено 26.08.2023.
Преглед/и станица
47
Протекла недеља
16
16
Протекли месец
0
0
проверено 10.05.2024.
Google ScholarTM
Проверите
Алт метрика
Ставке на DSpace-у су заштићене ауторским правима, са свим правима задржаним, осим ако није другачије назначено.