A Type System Equivalent to Flow Analysis

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.

I believe it's instructive to see type systems in this light. Did we discuss something like this recently?

By Andris Birkmanis at 2005-01-31 11:26 | Type Theory | other blogs | 5168 reads

Flow Caml

How does it relate to Flow Caml? IIRC we mentioned Flow Caml some times, but never as a topic.

By Daniel Yokomizo at Mon, 2005-01-31 13:30 | login or register to post comments

FC sees them as orthogonal not as equivalent

How does it relate to Flow Caml?

Funny that you ask, because I checked Flow Caml site just before posting that story.

AFAIK, Flow Caml uses flow analysis to infer/check security levels, which are orthogonal to ML type system. I am not sure whether Flow Caml does not use flow analysis to infer ML types.

OTOH, the equivalence paper I cited explicitly states that "we find that a type system and a flow analysis can in some cases be equivalent ways of looking at the same problem".

I might be wrong as my acquaintance with Flow Caml is pretty superficial.

By Andris Birkmanis at Mon, 2005-01-31 14:21 | login or register to post comments

OTOH, the equivalence paper I

OTOH, the equivalence paper I cited explicitly states that "we find that a type system and a flow analysis can in some cases be equivalent ways of looking at the same problem"

Well if we are going to look at different ways of looking at type systems: Types as Abstract Interpretations.

By Derek Elkins at Mon, 2005-01-31 14:47 | login or register to post comments

A calculus with polymorphic and polyvariant flow types

We present lambdaCIL, a typed lambda-calculus which serves as the foundation for a typed intermediate language for optimizing compilers for higher-order polymorphic programming languages. The key innovation of lambdaCIL is a novel formulation of intersection and union types and flow labels on both terms and types. These flow types can encode polyvariant control and data flow information within a polymorphically typed program representation. Flow types can guide a compiler in generating customized data representations in a strongly typed setting. Since lambdaCIL enjoys confluence, standardization, and subject reduction properties, it is a valuable tool for reasoning about programs and program transformations.

Or shorter: optimizing compilers that use dependent types internally :-)

By Andris Birkmanis at Tue, 2005-02-08 18:22 | login or register to post comments

Lambda the Ultimate

User login

Navigation