A type system equivalent to flow analysis
- 1 July 1995
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 17 (4) , 576-599
- https://doi.org/10.1145/210184.210187
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 article 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.Keywords
This publication has 7 references indexed in Scilit:
- Closure analysis in constraint formACM Transactions on Programming Languages and Systems, 1995
- Separate abstract interpretation for control-flow analysisPublished by Springer Nature ,1994
- Efficient analyses for realistic off-line partial evaluationJournal of Functional Programming, 1993
- A tour of SchismPublished by Association for Computing Machinery (ACM) ,1993
- Automatic autoprojection of higher order recursive equationsScience of Computer Programming, 1991
- Type inference for record concatenation and multiple inheritanceInformation and Computation, 1991
- Finding the source of type errorsPublished by Association for Computing Machinery (ACM) ,1986