Relational Reasoning for Programers using Higher-Order Store

The main aim of this project is to research new relational reasoning techniques for programming languages with features found in modern programming languages, in particular polymorphism and higher-order store (aka general references).

To develop correct and reliable software we need good formal reasoning methods for reasoning about programs written in modern programming languages. One of the most fundamental notions in formal reasoning about programs is contextual equivalence, which expresses when one program fragment may be interchanged by another fragment, without changing the overall meaning of a complete program. This is the notion of correctness that one is interested in when, e.g., proving compiler optimizations correct. Moreover, understanding contextual equivalence is, of course, a crucial ingredient in simply understanding the semantics of a programming language, and as such it forms the basis for other reasoning methods.