Transformer semantics

swMATH ID: 42013
Software Authors: Georg Struth
Description: afp Transformer_Semantics: Transformer Semantics. 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.
Homepage: https://www.isa-afp.org/entries/Transformer_Semantics.html
Dependencies: Isabelle
Related Software: Archive Formal Proofs; Quantales; KeYmaera X; Differential_Game_Logic; KAD; Algebraic_VCs; Kleene Algebra; Ordinary Differential Equations; Bellerophon; Coquelicot; C-CoRN; RODAS; KeYmaera; Isabelle/HOL
Cited in: 1 Document

Citations by Year