Geodesic
Idealized coinductive type systems for imperative object-oriented programs
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 1, pp. 3-33

Voir la notice de l'article provenant de la source Numdam

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.

DOI : 10.1051/ita/2011009
Classification : 03B70, 03B15
Keywords: imperative object-oriented languages, type analysis, coinduction, SSA intermediate form 
@article{ITA_2011__45_1_3_0,
     author = {Ancona, Davide and Lagorio, Giovanni},
     title = {Idealized coinductive type systems for imperative object-oriented programs},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {3--33},
     publisher = {EDP-Sciences},
     volume = {45},
     number = {1},
     year = {2011},
     doi = {10.1051/ita/2011009},
     mrnumber = {2776852},
     zbl = {1220.68047},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2011009/}
}
TY  - JOUR
AU  - Ancona, Davide
AU  - Lagorio, Giovanni
TI  - Idealized coinductive type systems for imperative object-oriented programs
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2011
SP  - 3
EP  - 33
VL  - 45
IS  - 1
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/articles/10.1051/ita/2011009/
DO  - 10.1051/ita/2011009
LA  - en
ID  - ITA_2011__45_1_3_0
ER  - 
%0 Journal Article
%A Ancona, Davide
%A Lagorio, Giovanni
%T Idealized coinductive type systems for imperative object-oriented programs
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2011
%P 3-33
%V 45
%N 1
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/articles/10.1051/ita/2011009/
%R 10.1051/ita/2011009
%G en
%F ITA_2011__45_1_3_0
Ancona, Davide; Lagorio, Giovanni. Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 1, pp. 3-33. doi: 10.1051/ita/2011009

Cité par Sources :