Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

DOI10.1017/S0960129500000414zbMath0809.03020OpenAlexW1966305152MaRDI QIDQ4302334

Frank Nordemann, Peter M. W. Knijnenburg

Publication date: 14 August 1994

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129500000414

zbMATH Keywords

axiomatizationlogic of partial termsHoare logicweakest precondition semanticsHoare triplescategory-theoretic semanticsalmost Heyting morphismscategorical model for first-order logicmorphisms between fibrespartial function logicpartial hyperdoctrinesweakest precondition functors

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Related Items (2)

Indexed and fibered structures for partial and total correctness assertions ⋮ Indexed and fibred structures for Hoare logic

Cites Work

• Notions of computation and monads
• A categorical treatment of pre- and post-conditions
• A note on undefined expression values in programming logics
• Categories of partial maps
• Conceptual completeness for first-order intuitionistic logic: An application of categorical logic
• Dominical categories: recursion theory without elements
• Tripos theory
• Ten Years of Hoare's Logic: A Survey—Part I
• Adjointness in Foundations
• An axiomatic basis for computer programming

This page was built for publication: Partial hyperdoctrines: categorical models for partial function logic and Hoare logic