Torben Amtoft and Franklyn Turbak.
Faithful Translations between Polyvariant Flows and Polymorphic Types.
Programming Languages and Systems: 9th European Symposium on Programming, ESOP 2000.
Published as Lecture Notes in Computer Science 1782 ,
Gert Smolka (Ed.)
Recent work has shown equivalences between various type systems and
flow logics. Ideally, the translations upon which such equivalences
are based should be faithful in the sense that information is
not lost in round-trip translations from flows to types and back or
from types to flows and back. Building on the work of Nielson and
Nielson and of Palsberg and Pavlopoulou, we present the first faithful
translations between a class of finitary polyvariant flow analyses and
a type system supporting polymorphism in the form of intersection and
union types. Additionally, our flow/type correspondence solves
several open problems posed by Palsberg and Pavlopoulou: (1) it
expresses call-string based polyvariance (such as k-CFA) as well as
argument based polyvariance; (2) it enjoys a subject reduction
property for flows as well as for types; and (3) it supports a
flow-oriented perspective rather than a type-oriented one.