Information flow inference for ML
Information flow inference for ML
复制标题
ML 的信息流推理
DOI：
10.1145/503272.503302
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Vincent Simonet
中科院分区：
文献类型：
--
作者：
F. Pottier;Vincent Simonet
本文提出了一种基于类型的基于值调用的λ演算的信息流分析方法，该演算具有引用、异常和let-多态功能。类型系统是基于约束的，并且具有可判定的类型推理。由于使用了许多正交技术，它的不干扰保护相当轻便。首先，值和表达式之间的语法分离允许更轻量级的类型系统。其次，对于非标准语言扩展，不干扰被简化为主语缩减。最后，类型合理性的半句法方法允许单独处理基于约束的多态。
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 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.