Молимо вас користите овај идентификатор за цитирање или овај линк до ове ставке:
https://open.uns.ac.rs/handle/123456789/13540
Назив: | Inhabitation in intersection and union type assignment systems | Аутори: | Gilezan, Silvia | Датум издавања: | 1-дец-1993 | Часопис: | Journal of Logic and Computation | Сажетак: | Union does not correspond to intuitionistic disjunction and intersection does not correspond to intuitionistic conjunction. The Curry-Howard isomorphism between types inhabited in the intersection and union type assignment system and formulae provable in intuitionistic propositional logic with implication, conjunction, disjunction and truth does not hold. This is shown semantically. The extension of the simply typed lambda calculus with conjunction and disjunction types and the corresponding elimination and introduction rules is considered. By the Curry-Howard isomorphism types inhabited in this extension of the simply typed lambda calculus correspond to the intuitionistically provable formulae. We shall link the inhabitation in the intersection and union type assignment system with the inhabitation in this extension of the simply typed lambda calculus. © Oxford University Press. | URI: | https://open.uns.ac.rs/handle/123456789/13540 | ISSN: | 0955792X | DOI: | 10.1093/logcom/3.6.671 |
Налази се у колекцијама: | FTN Publikacije/Publications |
Приказати целокупан запис ставки
SCOPUSTM
Навођења
2
проверено 09.09.2023.
Преглед/и станица
96
Протекла недеља
34
34
Протекли месец
5
5
проверено 03.05.2024.
Google ScholarTM
Проверите
Алт метрика
Ставке на DSpace-у су заштићене ауторским правима, са свим правима задржаним, осим ако није другачије назначено.