Lambda the Ultimate

Expressing Heap-shape Contracts in Linear Logic, Frances Perry, Limin Jia, David Walker.

Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation.

In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modifed version of LolliMon, a linear logic programming language.

This is a very elegant idea -- write assertions about heap shape using linear logic, and then check those assertions using a logic programming engine that traces the heap.

One thing this work reminds me is that I don't really understand the relationship between the way that they use the "with" connective (A & B) of linear logic and the way conjunction (A /\ B) is used in separation logic.