We present a relational model of an advanced type-and-effect system that validates advanced type-based equivalences, such as parallelization.

This paper examines the formal specification and verification of custom synchronisation constructs. Our target is a library of channels used in automated parallelization to enforce sequential behaviour between program statements.

Step-indexing is a powerful technique for stratifying the construction of recursive models of advanced type systems and logics. Current techniques enforce a tight coupling between concrete steps and unfoldings of this underlying recursive equation. We show how to weaken this coupling using transfinite step-indexing.

We present a program logic for a high-level programming language with a weak memory model that supports both low-level reasoning about racy code and high-level reasoning about well-behaved code.

We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce—user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.

We present a program logic for modular reasoning about safety properties of concurrent, higher-order, reentrant, imperative code.

We formally specify and verify a lock-based implementation of the C# Joins library using our HOCAP logic.

We present a spec. pattern for concurrent data structures that is independent of how clients intend to use instances of the data structure.

We present a new approach to admissibility for dependent type theories extended with partial types.

We present a program logic for a subset of C# that includes generics and anonymous delegates with variable capture.

We present separation logic specifications for a number of classic design patterns including the subject-observer pattern, the flyweight pattern and the iterator pattern.