A Relatively Complete Generic Hoare Logic for Order-Enriched Effects

DOI10.1109/LICS.2013.33zbMath1366.68023OpenAlexW1982145886WikidataQ130864089 ScholiaQ130864089MaRDI QIDQ5271064

Lutz Schröder, Sergei S. Goncharov

Publication date: 3 July 2017

Published in: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/lics.2013.33

zbMATH Keywords

monadsHoare logiccomputational effectsweakest preconditionsstrongest postconditions

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Continuous lattices and posets, applications (06B35) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Enriched categories (over closed or monoidal categories) (18D20)

Related Items (6)

Indexed and fibered structures for partial and total correctness assertions ⋮ Weakest preconditions in fibrations ⋮ Generic weakest precondition semantics from monads enriched with order ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Graded Hoare logic and its categorical semantics ⋮ Weakest preconditions in fibrations

This page was built for publication: A Relatively Complete Generic Hoare Logic for Order-Enriched Effects