A Type System Equivalent to Flow Analysis

A Type System Equivalent to Flow Analysis

Jens Palsberg
Patrick O'Keefe

In 6th NWPT, pages 300-316


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.

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 symbol] BRICS WWW home page