Predicate Transformers and Linear Logic, yet another denotational model
Logic in Computer Science
2009-05-26 v1 Logic
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.
Cite
@article{arxiv.0905.3998,
title = {Predicate Transformers and Linear Logic, yet another denotational model},
author = {Pierre Hyvernat},
journal= {arXiv preprint arXiv:0905.3998},
year = {2009}
}