|Authors:||Ghilezan, Silvia||Title:||Sound and complete subtyping on intersection and union types||Journal:||Book of Abstracts: Logics and Applications - LAP 2017||First page:||16||Last page:||17||Conference:||6th International Conference Logic and Applications 2017 - LAP 2017, 18-22 September 2017||Issue Date:||Sep-2017||Rank:||M34||URL:||http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP_2017_Book_of_Abstracts.pdf||Abstract:||
The notion of subtyping has gained an important role both in the oretical 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 in  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 present the technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types given in . An overview of preciseness of subtyping in other frameworks will be given (). This is a joint work with Mariangiola Dezani-Ciancaglini.
|Project:||Representations of logical structures and formal languages and their application in computing
Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education
Show full item record
checked on Feb 8, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.