In 6th NWPT, pages 300-316
In this paper we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.
Palsberg: BRICS, Department of Computer Science, University of Aarhus, DK-8000 Aarhus C, Denmark. Email: firstname.lastname@example.org. O'Keefe: 151 Coolidge Avenue # 211, Watertown, MA 02172, USA. Email: email@example.com.
Available as PostScript,