Please use this identifier to cite or link to this item: https://open.uns.ac.rs/handle/123456789/11319
DC FieldValueLanguage
dc.contributor.authorDownen P.en_US
dc.contributor.authorAriola Z.en_US
dc.contributor.authorGilezan, Silviaen_US
dc.date.accessioned2020-03-03T14:43:54Z-
dc.date.available2020-03-03T14:43:54Z-
dc.date.issued2019-01-01-
dc.identifier.issn1692968en_US
dc.identifier.urihttps://open.uns.ac.rs/handle/123456789/11319-
dc.description.abstract© 2019 - IOS Press and the authors. All rights reserved. For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest - soundness, completeness, and type safety - we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems - one for call-by-value and one for call-by-name evaluation - which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.en_US
dc.relation.ispartofFundamenta Informaticaeen_US
dc.titleThe Duality of Classical Intersection and Union Typesen_US
dc.typeJournal/Magazine Articleen_US
dc.identifier.doi10.3233/FI-2019-1855-
dc.identifier.scopus2-s2.0-85074327263-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/85074327263-
dc.description.versionUnknownen_US
dc.relation.lastpage92en_US
dc.relation.firstpage39en_US
dc.relation.issue1-3en_US
dc.relation.volume170en_US
item.fulltextNo Fulltext-
item.grantfulltextnone-
crisitem.author.deptDepartman za opšte discipline u tehnici-
crisitem.author.orcid0000-0003-2253-8285-
crisitem.author.parentorgFakultet tehničkih nauka-
Appears in Collections:FTN Publikacije/Publications
Show simple item record

SCOPUSTM   
Citations

3
checked on May 20, 2023

Page view(s)

88
Last Week
32
Last month
0
checked on May 3, 2024

Google ScholarTM

Check

Altmetric


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