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.
Publié le : 2004-09-20
Classification:
Predicate Transformers,
Linear Logic,
Denotational Semantics,
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO],
[MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
@article{hal-00387490,
author = {Hyvernat, Pierre},
title = {Predicate Transformers and Linear Logic, yet another denotational model},
journal = {HAL},
volume = {2004},
number = {0},
year = {2004},
language = {en},
url = {http://dml.mathdoc.fr/item/hal-00387490}
}
Hyvernat, Pierre. Predicate Transformers and Linear Logic, yet another denotational model. HAL, Tome 2004 (2004) no. 0, . http://gdmltest.u-ga.fr/item/hal-00387490/