Authors: Dezani-Ciancaglini, Mariangiola
Ghilezan, Silvia 
Title: Preciseness of subtyping on intersection and union types
Journal: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume: 8560 LNCS
First page: 194
Last page: 207
Conference: 25th International Conference on Rewriting Techniques and Applications, RTA 2014 and 12th International Conference on Typed Lambda Calculus and Applications, TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014; Vienna; Austria; 14 July 2014 through 17 July 2014
Issue Date: 1-Jan-2014
Rank: M33
ISBN: 978-3-319-08917-1
ISSN: 0302-9743
DOI: 10.1007/978-3-319-08918-8_14
Abstract: 
The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We then prove soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.
Publisher: Springer Link

Show full item record

SCOPUSTM   
Citations

7
checked on Nov 27, 2022

Page view(s)

13
checked on Nov 28, 2022

Google ScholarTM

Check

Altmetric

Altmetric


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