|
Transformer
Semantics
Title: |
Transformer Semantics |
Author:
|
Georg Struth
|
Submission date: |
2018-12-11 |
Abstract: |
These mathematical components formalise predicate transformer
semantics for programs, yet currently only for partial correctness and
in the absence of faults. A first part for isotone (or monotone),
Sup-preserving and Inf-preserving transformers follows Back and von
Wright's approach, with additional emphasis on the quantalic
structure of algebras of transformers. The second part develops
Sup-preserving and Inf-preserving predicate transformers from the
powerset monad, via its Kleisli category and Eilenberg-Moore algebras,
with emphasis on adjunctions and dualities, as well as isomorphisms
between relations, state transformers and predicate transformers. |
BibTeX: |
@article{Transformer_Semantics-AFP,
author = {Georg Struth},
title = {Transformer Semantics},
journal = {Archive of Formal Proofs},
month = dec,
year = 2018,
note = {\url{http://isa-afp.org/entries/Transformer_Semantics.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Order_Lattice_Props, Quantales |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|