Paper Info
Title
Idealized coinductive type systems for imperative object-oriented programs.
Abstract
In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas, where. functions correspond to union types.
Year
DOI
Venue
2011
10.1051/ita/2011009
RAIRO-THEORETICAL INFORMATICS AND APPLICATIONS
Keywords
Field
DocType
Imperative object-oriented languages,type analysis,coinduction,SSA intermediate form
Programming language,Union type,Object-oriented programming,Imperative programming,Horn function,Coinduction,Mathematics,Static single assignment form
Journal
Volume
Issue
ISSN
45
1
0988-3754
Citations 
PageRank 
References 
11
0.64
25
Authors
2
Name
Order
Citations
PageRank
Davide Ancona172769.43
Giovanni Lagorio221217.98