Idealized coinductive type systems for imperative object-oriented programs

Davide Ancona; Giovanni Lagorio

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2011)

  • Volume: 45, Issue: 1, page 3-33
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Ancona, Davide, and Lagorio, Giovanni. "Idealized coinductive type systems for imperative object-oriented programs." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 45.1 (2011): 3-33. <http://eudml.org/doc/273074>.

@article{Ancona2011,
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.},
author = {Ancona, Davide, Lagorio, Giovanni},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {imperative object-oriented languages; type analysis; coinduction; SSA intermediate form},
language = {eng},
number = {1},
pages = {3-33},
publisher = {EDP-Sciences},
title = {Idealized coinductive type systems for imperative object-oriented programs},
url = {http://eudml.org/doc/273074},
volume = {45},
year = {2011},
}

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
PB - EDP-Sciences
VL - 45
IS - 1
SP - 3
EP - 33
AB - 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.
LA - eng
KW - imperative object-oriented languages; type analysis; coinduction; SSA intermediate form
UR - http://eudml.org/doc/273074
ER -

References

top
  1. [1] O. Agesen, The cartesian product algorithm, in ECOOP'05 – Object-Oriented Programming. Lecture Notes in Computer Science 952 (1995) 2–26. 
  2. [2] R. Amadio and L. Cardelli, Subtyping recursive types. ACM Trans. Prog. Lang. Syst.15 (1993) 575–631. 
  3. [3] D. Ancona and G. Lagorio, Coinductive type systems for object-oriented languages, in ECOOP'09 – Object-Oriented Programming. Lecture Notes in Computer Science 5653 (2009) 2–26. 
  4. [4] D. Ancona and G. Lagorio, Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas, in Proceedings of GandALF 2010. Electronic Proceedings in Theoretical Computer Science 25 (2010) 214–223. 
  5. [5] D. Ancona and G. Lagorio, Complete coinductive subtyping for abstract compilation of object-oriented languages, in Formal Techniques for Java-like Programs (FTfJP10), ACM Digital Library (2010). 
  6. [6] D. Ancona, G. Lagorio and E. Zucca, Type inference for polymorphic methods in Java-like languages, in ICTCS'07 – Italian Conf. on Theoretical Computer Science, edited by G.F. Italiano, E. Moggi and L. Laura, eProceedings. World Scientific (2007). 
  7. [7] D. Ancona, G. Lagorio and E. Zucca, Type inference by coinductive logic programming, in Post-Proceedings of TYPES'08. Lecture Notes in Computer Science 5497 (2009). Zbl1246.68079MR2544188
  8. [8] D. Ancona, A. Corradi, G. Lagorio and F. Damiani, Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification. Technical report, Karlsruhe Institute of Technology (2010). Formal Verification of Object-Oriented Software. Papers presented at the International Conference, Paris, France (2010). Zbl1308.68027
  9. [9] C. Anderson, P. Giannini and S. Drossopoulou, Towards type inference for Javascript, in ECOOP'05 – Object-Oriented Programming. Lecture Notes in Computer Science 3586 (2005) 428–452. 
  10. [10] F. Barbanera, M. Dezani-Cincaglini and U. de'Liguoro, Intersection and union types: Syntax and semantics. Inform. Comput. 119 (1995) 202–230. Zbl0832.68065MR1334464
  11. [11] W.R. Cook, W.L. Hill and P.S. Canning, Inheritance is not subtyping, in ACM Symp. on Principles of Programming Languages 1990. ACM Press (1990), 125–135. Zbl0837.68061
  12. [12] B. Courcelle, Fundamental properties of infinite trees. Theoret. Comput. Sci.25 (1983) 95–169. Zbl0521.68013MR693076
  13. [13] P. Cousot, Types as abstract interpretations, in ACM Symp. on Principles of Programming Languages (1997), 316–331. 
  14. [14] P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in ACM Symp. on Principles of Programming Languages 1977. ACM Press (1977), 238–252. 
  15. [15] R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman and F.K. Zadeck, Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Prog. Lang. Syst.13 (1991) 451–490. 
  16. [16] D. Das and U. Ramakrishna, A practical and fast iterative algorithm for phi-function computation using DJ graphs. ACM Trans. Prog. Lang. Syst.27 (2005) 426–440. 
  17. [17] M. Furr, J. An, J.S. Foster and M. Hicks, Static type inference for Ruby, in SAC '09: Proceedings of the 2009 ACM symposium on Applied computing. ACM Press (2009). 
  18. [18] P. Heidegger and P. Thiemann, Recency types for analyzing scripting languages, in ECOOP'10 – Object-Oriented Programming. Lecture Notes in Computer Science 6183 (2010) 200–224. 
  19. [19] A. Igarashi and H. Nagira, Union types for object-oriented programming. JOT6 (2007) 47–68. 
  20. [20] A. Igarashi, B.C. Pierce and P. Wadler, Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst.23 (2001) 396–450. 
  21. [21] X. Leroy and H. Grall, Coinductive big-step operational semantics. Inform. Comput.207 (2009) 284–304. Zbl1165.68044MR2498711
  22. [22] R. Min and G. Gupta, Coinductive logic programming and its application to boolean sat, in FLAIRS Conference (2009). Zbl1213.68177
  23. [23] R. Min and G. Gupta, Coinductive logic programming with negation, in LOPSTR (2009), 97–112. Zbl1284.68117MR2754598
  24. [24] N. Oxhøj, J. Palsberg and M.I. Schwartzbach, Making type inference practical, in ECOOP'92 – European Conference on Object-Oriented Programming (1992), 329–349. 
  25. [25] M. Odersky, M. Sulzmann and M. Wehr, Type inference with constrained types. Theory Pract. Obj. Syst.5 (1999) 35–55. 
  26. [26] J. Palsberg and M.I. Schwartzbach, Object-oriented type inference, in ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1991. ACM Press (1991), 146–161. 
  27. [27] J. Palsberg and M.I. Schwartzbach, Object-Oriented Type Systems. John Wiley & Sons (1994). Zbl0821.68023
  28. [28] J. Plevyak and A. Chien, Precise concrete type inference for object-oriented languages, in Ninth Annual ACM Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM Press (1994), 324–340. 
  29. [29] N. Saeedloei and G. Gupta, Verifying complex continuous real-time systems with coinductive CLP(R), in Proc. of LATA 2010. Lecture Notes in Computer Science (2010). Zbl1284.68365MR2753938
  30. [30] L. Simon, A. Mallya, A. Bansal and G. Gupta, Coinductive logic programming, in Logic Programming, 22nd International Conference, ICLP (2006), 330–345. Zbl1131.68400
  31. [31] L. Simon, A. Bansal, A. Mallya and G. Gupta, Co-logic programming: Extending logic programming with coinduction, in Automata, Languages and Programming, 34th International Colloquium, ICALP (2007), 472–483. Zbl1171.68404MR2424706
  32. [32] J. Singer, Static Program Analysis based on Virtual Register Renaming, Ph.D. thesis, Computer Laboratory, University of Cambridge (2006). 
  33. [33] M. Sulzmann and P.J. Stuckey, HM(X) type inference is CLP(X) solving. J. Funct. Program.18 (2008) 251–283. Zbl1142.68021MR2413646
  34. [34] T. Wang and S.F. Smith, Precise constraint-based type inference for Java, in ECOOP'01 – European Conference on Object-Oriented Programming 2072 (2001) 99–117. Zbl0982.68729
  35. [35] T. Wang and S. Smith, Polymorphic constraint-based type inference for objects. Technical report, The Johns Hopkins University (2008), submitted for publication. 
  36. [36] T. Zhao, Type inference for scripting languages with implicit extension, in FOOL 2010 – Intl. Workshop on Foundations of Object-Oriented Languages (2010). 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.