Frame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Charguéraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised tofamiliesof invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S.

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguéraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.

Abstract One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A ≤ B are interpreted via conversion functions A → B . This paper shows how to extend the method to languages with computational effects, using Moggi's computational metalanguage.

The object-calculus is an imperative and object-based programming language in which every object comes equipped with its own method suite. Consequently, methods need to reside in the store (‘higher-order store’), which complicates the semantics. Abadi and Leino defined a program logic for this language enriching object types by method specifications. We present a new soundness proof for their logic using denotational semantics. It turns out that denotations of store specifications are predicates defined by mixed-variant recursion. A benefit of our approach is that derivability and validity can be kept distinct. Moreover, it reveals which of the limitations of Abadi and Leino's logic are incidental design decisions and which follow inherently from the use of a higher-order store. We discuss the implications for the development of other, more expressive, program logics.