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
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 [3] 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 [1]. An overview of preciseness of subtyping in other frameworks will be given ([2]). 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

Page view(s)

checked on May 9, 2024

Google ScholarTM


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