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

DOI10.1017/S0960129500000414MaRDI QIDQ4302334zbMATH OpenOpenAlexFDO

Authors 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

almost Heyting morphismsaxiomatizationcategorical model for first-order logiccategory-theoretic semanticsHoare logicHoare tripleslogic of partial termsmorphisms between fibrespartial function logicpartial hyperdoctrinesweakest precondition functorsweakest precondition semantics

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1678378
• scientific article; zbMATH DE number 3999922
• Partial Horn logic and Cartesian categories
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• scientific article; zbMATH DE number 1722655
• Categorical models for non-extensional λ-calculi and combinatory logic
• Categorical models for Abadi and Plotkin's logic for parametricity
• Category-theoretic models of linear Abadi \& Plotkin logic
• Paraconsistent categories for paraconsistent logics
• Classifying categories for partial equational logic

Cites work

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

Cited in

(7)

• Indexed and fibred structures for Hoare logic
• scientific article; zbMATH DE number 1678378 (Why is no real title available?)
• Full Lambek Hyperdoctrine: Categorical Semantics for First-Order Substructural Logics
• A general framework for sound and complete Floyd-Hoare logics
• Hoare Logic in the Abstract
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Indexed and fibered structures for partial and total correctness assertions

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

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