[24]
demonstrates that there is a close relationship between
polyvariant flow analyses and type systems with finitary polymorphism.
We present a flow logic, based on the general approach
of Nielson & Nielson
and augmented with ideas from Palsberg & Pavlopoulou,
and also present a type system employing
union and intersection types;
both these systems satisfy a subject reduction property.
We then provide translations between types and flows
that are “faithful” in that they act as the identity on “canonical”
elements, and otherwise canonicalize.
