Predicate Transformers and Linear Logic, yet another denotational model

TL;DR

This paper develops a denotational model of full linear logic using predicate transformers from the refinement calculus, interpreting logical constructs as specifications and proofs as safety properties.

Contribution

It introduces a novel categorical model of linear logic based on predicate transformers, linking logical proofs to safety properties in specifications.

Findings

Predicate transformers form a category with algebraic properties.

Logical constructions are naturally interpreted as specifications.

Proofs correspond to safety properties of specifications.

Abstract

In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic properties. We build on this structure to make predicate transformers into a de notational model of full linear logic: all the logical constructions have a natural interpretation in terms of predicate transformers (i.e. in terms of specifications). We then interpret proofs of a formula by a safety property for the corresponding specification.