Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
Copyright policy )Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
In this paper we provide a categorical interpretation of the first-order Hoare logic of a small programming language by giving a weakest precondition semantics for the language. To this end, we extend the well-known notion of a (first-order) hyperdoctrine to include partial maps. The most important new aspect of the resulting partial (first-order) hyperdoctrine is a different notion of morphism between the fibres. We also use this partial hyperdoctrine to give a model for Beeson's Partial Function Logic such that (a version of) his axiomatization is complete with respect to this model. This shows the usefulness of the notion, independent of its intended use as a model for Hoare logic.
- Utrecht University Netherlands
category-theoretic semantics, Logic in computer science, Hoare triples, Semantics in the theory of computing, categorical model for first-order logic, Hoare logic, almost Heyting morphisms, Theories (e.g., algebraic theories), structure, and semantics, weakest precondition semantics, morphisms between fibres, partial function logic, partial hyperdoctrines, axiomatization, logic of partial terms, weakest precondition functors, Categorical logic, topoi
category-theoretic semantics, Logic in computer science, Hoare triples, Semantics in the theory of computing, categorical model for first-order logic, Hoare logic, almost Heyting morphisms, Theories (e.g., algebraic theories), structure, and semantics, weakest precondition semantics, morphisms between fibres, partial function logic, partial hyperdoctrines, axiomatization, logic of partial terms, weakest precondition functors, Categorical logic, topoi
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).1 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!