Information flow inference for ML
Information flow inference for ML
复制标题
DOI：
10.1145/565816.503302
复制
发表时间：
2002-01-01
影响因子：
--
通讯作者：
Simonet, V
中科院分区：
文献类型：
--
作者：
Pottier, F;Simonet, V
本文提出了一种基于类型的信息流分析方法，用于分析带有引用、异常和let多态的按值调用的lambda演算，我们称之为Core ML。类型系统是基于约束的，并且具有可判定的类型推理。由于使用了许多正交技术，它的不干扰保护相当轻便。首先，值和表达式之间的语法分离允许更轻量级的类型系统。其次，对于非标准语言扩展，不干扰被简化为主语缩减。最后，类型合理性的半句法方法允许单独处理基于约束的多态。
This paper presents a type-based information flow analysis for a call-by-value lambda-calculus equipped with references, exceptions and let-polymorphism, which we refer to as Core ML. The type system is constraint-based and has decidable type inference. Its non-interference proof is reasonably lightweight, 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, non-interference is reduced to subject reduction for a non-standard language extension. Lastly, a semi-syntactic approach to type soundness allows dealing with constraint-based polymorphism separately.