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

DOI10.1017/S0960129500000414zbMath0809.03020MaRDI QIDQ4302334

Frank Nordemann, Peter M. W. Knijnenburg

Publication date: 14 August 1994

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

zbMATH Keywords

axiomatization; logic of partial terms; Hoare logic; weakest precondition semantics; Hoare triples; category-theoretic semantics; almost Heyting morphisms; categorical model for first-order logic; morphisms between fibres; partial function logic; partial hyperdoctrines; weakest precondition functors

Mathematics Subject Classification ID

03B70: Logic in computer science

68Q55: Semantics in the theory of computing

03G30: Categorical logic, topoi

18C10: Theories (e.g., algebraic theories), structure, and semantics

Related Items

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