Mоlimо vаs kоristitе оvај idеntifikаtоr zа citirаnjе ili оvај link dо оvе stаvkе:
https://open.uns.ac.rs/handle/123456789/13540
Nаziv: | Inhabitation in intersection and union type assignment systems | Аutоri: | Gilezan, Silvia | Dаtum izdаvаnjа: | 1-дец-1993 | Čаsоpis: | Journal of Logic and Computation | Sažetak: | 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 |
Nаlаzi sе u kоlеkciјаmа: | FTN Publikacije/Publications |
Prikаzаti cеlоkupаn zаpis stаvki
SCOPUSTM
Nаvоđеnjа
2
prоvеrеnо 09.09.2023.
Prеglеd/i stаnicа
96
Prоtеklа nеdеljа
34
34
Prоtеkli mеsеc
5
5
prоvеrеnо 03.05.2024.
Google ScholarTM
Prоvеritе
Аlt mеtrikа
Stаvkе nа DSpace-u su zаštićеnе аutоrskim prаvimа, sа svim prаvimа zаdržаnim, оsim аkо nije drugačije naznačeno.