A Kripke Logical Relation for Effect-Based Program Transformations

作者：Tham**org Jacob^*; Birkedal Lars

来源：ACM Sigplan Notices, 2011, 46(9): 445-456.

DOI：10.1145/2034574.2034831

• Languages
• Theory
• Verification
• Kripke logical relation
• ultrametric spaces
• step-indexed model
• type and effect system
• program transformations
• effect masking
• dangling pointers

We present a Kripke logical relation for showing the correctness of program transformations based on a type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation.
We show how to use our model to verify a number of interesting program transformations that rely on effect annotations.
Our model is constructed as a step-indexed model over the standard operational semantics of the programming language. It extends earlier work [7, 8] that has considered, respectively, dynamically allocated first-order references and higher-order store for global variables (but no dynamic allocation). It builds on ideas from region-based memory management [21], and on Kripke logical relations for higher-order store, e. g. [12, 14].
Our type-and-effect system is region-based and includes a region-masking rule which allows to hide local effects. One of the key challenges in the model construction for dynamically allocated higher-order store is that the meaning of a type may change since references, conceptually speaking, may become dangling due to region-masking. We explain how our Kripke model can be used to show correctness of program transformations for programs involving references that, conceptually, are dangling.

• 出版日期2011-9