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 Cited by 2 Authors 1 Huerta y Munive, Jonathan Julián 1 Struth, Georg Cited in 1 Serial 1 Journal of Automated Reasoning Cited in 1 Field 1 Computer science (68-XX) Citations by Year