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.

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}, publisher = {EDP-Sciences}, volume = {45}, number = {1}, year = {2011}, pages = {3-33}, doi = {10.1051/ita/2011009}, zbl = {1220.68047}, mrnumber = {2776852}, language = {en}, url = {http://www.numdam.org/item/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, Volume 45 (2011) no. 1, pp. 3-33. doi : 10.1051/ita/2011009. http://www.numdam.org/item/ITA_2011__45_1_3_0/

[1] The cartesian product algorithm, in ECOOP'05 - Object-Oriented Programming. Lecture Notes in Computer Science 952 (1995) 2-26.

,[2] Subtyping recursive types. ACM Trans. Prog. Lang. Syst. 15 (1993) 575-631.

and ,[3] Coinductive type systems for object-oriented languages, in ECOOP'09 - Object-Oriented Programming. Lecture Notes in Computer Science 5653 (2009) 2-26.

and ,[4] 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.

and ,[5] Complete coinductive subtyping for abstract compilation of object-oriented languages, in Formal Techniques for Java-like Programs (FTfJP10), ACM Digital Library (2010).

and ,[6] 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).

, and ,[7] Type inference by coinductive logic programming, in Post-Proceedings of TYPES'08. Lecture Notes in Computer Science 5497 (2009). | MR 2544188 | Zbl 1246.68079

, and ,[8] 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). | Zbl pre05839896

, , and ,[9] Towards type inference for Javascript, in ECOOP'05 - Object-Oriented Programming. Lecture Notes in Computer Science 3586 (2005) 428-452.

, and ,[10] F. Barbanera, M. Dezani-Cincaglini and U. de'Liguoro, Intersection and union types: Syntax and semantics. Inform. Comput. 119 (1995) 202-230. | MR 1334464 | Zbl 0832.68065

[11] Inheritance is not subtyping, in ACM Symp. on Principles of Programming Languages 1990. ACM Press (1990), 125-135. | Zbl 0837.68061

, and ,[12] Fundamental properties of infinite trees. Theoret. Comput. Sci. 25 (1983) 95-169. | MR 693076 | Zbl 0521.68013

,[13] Types as abstract interpretations, in ACM Symp. on Principles of Programming Languages (1997), 316-331.

,[14] 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.

and ,[15] Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Prog. Lang. Syst. 13 (1991) 451-490.

, , , and ,[16] A practical and fast iterative algorithm for phi-function computation using DJ graphs. ACM Trans. Prog. Lang. Syst. 27 (2005) 426-440.

and ,[17] 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] Recency types for analyzing scripting languages, in ECOOP'10 - Object-Oriented Programming. Lecture Notes in Computer Science 6183 (2010) 200-224.

and ,[19] Union types for object-oriented programming. JOT 6 (2007) 47-68.

and ,[20] Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst. 23 (2001) 396-450.

, and ,[21] Coinductive big-step operational semantics. Inform. Comput. 207 (2009) 284-304. | MR 2498711 | Zbl 1165.68044

and ,[22] Coinductive logic programming and its application to boolean sat, in FLAIRS Conference (2009). | Zbl 1213.68177

and ,[23] Coinductive logic programming with negation, in LOPSTR (2009), 97-112. | MR 2754598 | Zbl 1284.68117

and ,[24] Making type inference practical, in ECOOP'92 - European Conference on Object-Oriented Programming (1992), 329-349.

, and ,[25] Type inference with constrained types. Theory Pract. Obj. Syst. 5 (1999) 35-55.

, and ,[26] Object-oriented type inference, in ACM Symp. on Object-Oriented Programming: Systems, Languages and Applications 1991. ACM Press (1991), 146-161.

and ,[27] Object-Oriented Type Systems. John Wiley & Sons (1994). | Zbl 0821.68023

and ,[28] 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.

and ,[29] Verifying complex continuous real-time systems with coinductive CLP(R), in Proc. of LATA 2010. Lecture Notes in Computer Science (2010). | MR 2753938 | Zbl 1284.68365

and ,[30] Coinductive logic programming, in Logic Programming, 22nd International Conference, ICLP (2006), 330-345. | Zbl 1131.68400

, , and ,[31] Co-logic programming: Extending logic programming with coinduction, in Automata, Languages and Programming, 34th International Colloquium, ICALP (2007), 472-483. | MR 2424706 | Zbl 1171.68404

, , and ,[32] Static Program Analysis based on Virtual Register Renaming, Ph.D. thesis, Computer Laboratory, University of Cambridge (2006).

,[33] HM(X) type inference is CLP(X) solving. J. Funct. Program. 18 (2008) 251-283. | MR 2413646 | Zbl 1142.68021

and ,[34] Precise constraint-based type inference for Java, in ECOOP'01 - European Conference on Object-Oriented Programming 2072 (2001) 99-117. | Zbl 0982.68729

and ,[35] Polymorphic constraint-based type inference for objects. Technical report, The Johns Hopkins University (2008), submitted for publication.

and ,[36] Type inference for scripting languages with implicit extension, in FOOL 2010 - Intl. Workshop on Foundations of Object-Oriented Languages (2010).

,