Healthiness from Duality

DOI10.1145/2933575.2935319MaRDI QIDQ4635931zbMATH OpenOpenAlexFDO

Authors Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo, Bart Jacobs

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.00381, http://hdl.handle.net/2066/161285

zbMATH Keywords

category theorydualityprogram logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Theories (e.g., algebraic theories), structure, and semantics (18C10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Healthiness is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic characterization of those predicate transformers which arise as the (backward) interpretation of a certain class of programs. There are several results known for healthiness conditions: for deterministic programs, nondeterministic ones, probabilistic ones, etc. Building upon our previous works on so-called state-and-effect triangles, we contribute a unified categorical framework for investigating healthiness conditions. We find the framework to be centered around a dual adjunction induced by a dualizing object, together with our notion of relative Eilenberg-Moore algebra playing fundamental roles too. The latter notion seems interesting in its own right in the context of monads, Lawvere theories and enriched categories.

Recommendations

• Dualities
• Duality and tameness
• scientific article; zbMATH DE number 1588513
• Many Facets of Dualities
• Anatomy of a duality.
• On the unity of duality
• scientific article; zbMATH DE number 802720
• A double look at duality

Cited in

(11)

• Steps and traces
• Weakest preconditions in fibrations
• Stone-type dualities for separation logics
• scientific article; zbMATH DE number 2079822 (Why is no real title available?)
• A unified framework for notions of algebraic theory
• Weakest preconditions in fibrations
• A recipe for state-and-effect triangles
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Healthiness conditions for predicate transformers
• A no-go theorem for coalgebraic product construction
• Probabilistic predicate transformers. II: Partially observable probability

This page was built for publication: Healthiness from Duality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635931)