Predicate Transformers and Linear Logic: Yet Another Denotational Model

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 denotational 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.

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Pierre Hyvernat
• Keywords: CSL 2004, Monotonic Predicate Transformers, Natural Notion, Predicate Transformers