A Type System Equivalent to Flow Analysis

Abstract

Flow-baaed safety analysis of higher-order languages has been studied by Shivers. and Palsberg and Schwartzbach. Open untd now M the problem of finding a type system that accepts exactly the same programs as safety analysis. In this article we prove that Amadio and Cardelli's type system with sub typing and recurmve t ypes accepts the same programs as a cert am safety analysls. The proof involves mappings from types to flow mformatlon and back. As a result. we obtain an inference algorithm for the type system, thereby solving an open problem. © 1995, ACM. All rights reserved.