A Kripke logical relation for effect-based program transformations

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review


We present a Kripke logical relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In building the model, we extend earlier work by Benton et al. that treated, respectively dynamically allocated first-order references, and higher-order store for global variables. We utilize ideas from region-based memory management, and on Kripke logical relations for higher-order store. One of the key challenges that we overcome in the construction of the model is treatment of masking of regions (conceptually similar to deallocation). Our approach bears similarities to the one used in Ahmed's unary model of a region calculus in her Ph.D. thesis.

Original languageEnglish
JournalInformation and Computation
Pages (from-to)160-189
Number of pages30
Publication statusPublished - Aug 2016

    Research areas

  • Effect type system, Kripke logical relation, Program transformation

See relations at Aarhus University Citationformats

ID: 108756530