Advances in Reasoning Principles for Contextual Equivalence and Termination

In this PhD Dissertation we develop methods for proving contextual equivalence
and termination. Contextual equivalence. We present three papers on contextual equivalence. All three share a common setup: They are based on an FM-denotational model with a parameterized admissible Kripke-style logical relation on top of a universal recursive domain. The combination of expressible parameters and a recursive domain makes it non-trivial to establish the existence of the relations, and this has required some new ideas. Our method is the first proof method for contextual equivalence based on a logical relation over a denotational semantics for a language with recursive types and dynamic allocation of references of any type. The first paper gives the general setup. The second paper gives a relationally parametric interpretation of polymorphic types. This is not quite as general as we would like; we restrict the type of references so that the type must be closed. It is to our knowledge the first relationally parametric model for higherorder store and polymorphic and recursive types. The third paper is primarily concerned with refining the definition of parameters. Termination analysis. In the last paper in the thesis we develop a sound and fully-automated algorithm to show that evaluation of a given untyped λexpression will terminate under call-by-value. The “size-change principle” from first-order programs is extended to arbitrary untyped λ-expressions in two steps. The first step suffices to show call-by-value termination of a single, stand-alone λ expression. The second suffices to show termination of any member of a regular set of λ-expressions, defined by a tree grammar.