Intersection and union types in the λ̄μμ̃-calculus

Dougherty, Daniel; Ghilezan, Silvia; Lescanne, Pierre

DC Field	Value	Language
dc.contributor.author	Dougherty, Daniel	en
dc.contributor.author	Ghilezan, Silvia	en
dc.contributor.author	Lescanne, Pierre	en
dc.date.accessioned	2020-05-02T16:42:22Z	-
dc.date.available	2020-05-02T16:42:22Z	-
dc.date.issued	2005-07-19	en
dc.identifier.issn	1571-0661	en
dc.identifier.uri	http://researchrepository.mi.sanu.ac.rs/handle/123456789/2607	-
dc.description.abstract	The original λ̄μμ̃ of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of λ̄μμ̃ with intersection and union types. The intrinsic symmetry in the λ̄μ μ̃ calculus leads to an essential use of both intersection and union types.	en
dc.publisher	Elsevier	-
dc.relation.ispartof	Electronic Notes in Theoretical Computer Science	en
dc.subject	Classical logic \| Curry-Howard correspondence \| Intersection types \| Union types \| λ̄μμ̃-calculus	en
dc.title	Intersection and union types in the λ̄μμ̃-calculus	en
dc.type	Conference Paper	en
dc.relation.conference	3rd International Workshop on intersection Types and Related Systems; 13 July 2004 through 13 July 2004	-
dc.identifier.doi	10.1016/j.entcs.2005.06.010	en
dc.identifier.scopus	2-s2.0-21744460433	en
dc.relation.firstpage	153	en
dc.relation.lastpage	172	en
dc.relation.volume	136	en
item.fulltext	No Fulltext	-
item.openairetype	Conference Paper	-
item.grantfulltext	none	-
item.cerifentitytype	Publications	-
item.openairecristype	http://purl.org/coar/resource_type/c_18cf	-
crisitem.author.orcid	0000-0003-2253-8285	-