A Type System Equivalent to Flow Analysis

Jens Palsberg
Patrick O'Keefe

In 6th NWPT, pages 300-316

Abstract:

Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis.

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.

Comments
Palsberg: BRICS, Department of Computer Science, University of Aarhus, DK-8000 Aarhus C, Denmark. Email: palsberg@daimi.aau.dk. O'Keefe: 151 Coolidge Avenue # 211, Watertown, MA 02172, USA. Email: pmo@world.std.com.

Available as PostScript, DVI.

BRICS WWW home page