Information flow inference for ML
Authors:
Open Access
- 1 January 2003
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 25 (1) , 117-158
Abstract
This paper presents a type-based information flow analysis for a call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as ML. The type system is constraint-based and has decidable type inference. Its noninterference proof is reasonably light-weight, thanks to the use of a number of orthogonal techniques. First, a syntactic segregation between values and expressions allows a lighter formulation of the type system. Second, noninterference is reduced to subject reduction for a nonstandard language extension. Lastly, a semi-syntactic approach to type soundness allows dealing with constraint-based polymorphism separately.Keywords
This publication has 15 references indexed in Scilit:
- JFlow1999
- A core calculus of dependency1999
- The SLam calculus1998
- Minimal typings in atomic subtyping1997
- Analysis and caching of dependencies1996
- Simple imperative polymorphismHigher-Order and Symbolic Computation, 1995
- A Syntactic Approach to Type SoundnessInformation and Computation, 1994
- The essence of compiling with continuations1993
- Comprehending monadsMathematical Structures in Computer Science, 1992
- Incremental reduction in the lambda calculus1990