Type systems equivalent to data-flow analyses for imperative languages

详细信息    查看全文

• 作者：Peeter Laud ; Tarmo Uustalu and Varmo Vene
• 刊名：Theoretical Computer Science
• 出版年：2006
• 出版时间：8 November 2006
• 年：2006
• 卷：364
• 期：3
• 页码：292-310
• 全文大小：453 K

文摘

We show that a large class of data-flow analyses for imperative languages are describable as type systems in the following technical sense: possible results of an analysis can be described in a language of types so that a program checks with a type if and only if this type is a supertype of the result of applying the analysis. Type-checking is easy with the help of a certificate that records the “eureka”-bits of a typing derivation. Certificate-assisted type-checking amounts to a form of lightweight analysis à la Rose. For secure information flow, we obtain a type system that is considerably more precise than that of Volpano et al., but not more sophisticated. Importantly, our type systems are compositional.