@proceedings {CominiDV07, title = {On Polymorphic Recursion, Type Systems, and Abstract Interpretation}, journal = {Static Analysis {\textendash} 15th International Symposium, SAS 2008}, volume = {5079}, year = {2008}, pages = {144{\textendash}158}, publisher = {Springer-Verlag}, address = {Berlin}, abstract = {The problem of typing polymorphic recursion (i.e. recursive function definitions rec{x = e} where different occurrences of x in e are used with different types) has been investigated both by people working on type systems and by people working on abstract interpretation. Recently, Gori and Levi have developed an abstract interpreter that is able to type all the ML typable recursive definitions and interesting examples of polymorphic recursion. The problem of finding a type system corresponding to their abstract interpreter was open. In this paper we present a type system corresponding to the Gori-Levi abstract interpreter. Interestingly enough, the type system is derived from the system of simple types (which is the let-free fragment of the ML type system) by adapting a general technique for extending a decidable type system enjoying principal typings by adding a decidable rule for typing recursive definitions. The key role played in our investigation by the notion of principal typing suggests that this notion might be useful in other investigations about the relations between type systems and type inference algorithms synthesized by abstract interpretation.}, author = {Marco Comini and Ferruccio Damiani and Samuel Vrech}, editor = {Maria Alpuente and Germ{\'a}n Vidal} }