|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.
Show full item record
checked on Mar 27, 2023
checked on Mar 28, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.