Paper Info
Title
Complete coinductive subtyping for abstract compilation of object-oriented languages
Abstract
Coinductive abstract compilation is a novel technique, which has been recently introduced, for defining precise type systems for object-oriented languages. In this approach, type inference consists in translating the program to be analyzed into a Horn formula f, and in resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of f. Type systems defined in this way are idealized, since types and, consequently, goal derivations, are not finitely representable. Hence, sound implementable approximations have to rely on the notions of regular types and derivations, and of subtyping and subsumption between types and atoms, respectively. In this paper we address the problem of defining a complete subtyping relation ≤ between types built on object and union type constructors: we interpret types as sets of values, and investigate on a definition of subtyping such that t1 ≤ t2 is derivable whenever the interpretation of t1 is contained in the interpretation of t2. Besides being an important theoretical result, completeness is useful for reasoning about possible implementations of the subtyping relation, when restricted to regular types.
Year
DOI
Venue
2010
10.1145/1924520.1924521
FTfJP@ECOOP
Field
DocType
Citations 
Covariance and contravariance,Union type,Programming language,Object-oriented programming,Computer science,Type inference,Coinduction,System F-sub,Subtyping,Completeness (statistics)
Conference
6
PageRank 
References 
Authors
0.47
15
2
Name
Order
Citations
PageRank
Davide Ancona172769.43
Giovanni Lagorio221217.98