{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,19]],"date-time":"2022-09-19T09:50:08Z","timestamp":1663581008674},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5390,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1994,6]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129500000414","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T04:01:15Z","timestamp":1236139275000},"page":"117-146","source":"Crossref","is-referenced-by-count":1,"title":["Partial hyperdoctrines: categorical models for partial function logic and Hoare logic"],"prefix":"10.1017","volume":"4","author":[{"given":"Peter","family":"Knijnenburg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Nordemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000414_ref022","volume-title":"Applications of Sheaves","author":"Scott","year":"1979"},{"key":"S0960129500000414_ref019","volume-title":"Higher Order Workshop, Banff 1990","author":"Pitts","year":"1990"},{"key":"S0960129500000414_ref016","unstructured":"Obtulowicz A. (1986) The logic of categories of partial functions and its applications. Dissertationes Mathematicae, CCXLI Pa\u0144stwowe Wydawnictwo Naukowe."},{"key":"S0960129500000414_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0960129500000414_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066201"},{"key":"S0960129500000414_ref003","volume-title":"Handbook of Theoretical Computer Science","author":"Cousot","year":"1990"},{"key":"S0960129500000414_ref013","first-page":"1","volume-title":"Proc. New York Symp. on Applications of Categorical Algebra","author":"Lawvere","year":"1970"},{"key":"S0960129500000414_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90158-X"},{"key":"S0960129500000414_ref012","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129500000414_ref018","unstructured":"Pitts A. M. (1989b) Notes on categorical logic. Technical report, Computer Laboratory, University of Cambridge."},{"key":"S0960129500000414_ref010","volume-title":"Stone Spaces","author":"Johnstone","year":"1982"},{"key":"S0960129500000414_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200029649"},{"key":"S0960129500000414_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90034-X"},{"key":"S0960129500000414_ref009","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100057534"},{"key":"S0960129500000414_ref002","first-page":"51","volume-title":"Logic, Methodology and Philosophy of Science VII","author":"Beeson","year":"1986"},{"key":"S0960129500000414_ref005","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"S0960129500000414_ref006","volume-title":"Categories, Allegories","author":"Freyd","year":"1991"},{"key":"S0960129500000414_ref024","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Van Dalen","year":"1988"},{"key":"S0960129500000414_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90025-9"},{"key":"S0960129500000414_ref008","first-page":"373","article-title":"On partial algebras","volume":"29","author":"Hoehnke","year":"1977","journal-title":"Colloq. Math. Soc. J\u00e1nos Bolyai"},{"key":"S0960129500000414_ref021","unstructured":"Rosolini G. (1986) Continuity and effectiveness in topoi, PhD thesis, Univ. of Oxford."},{"key":"S0960129500000414_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(89)90007-9"},{"key":"S0960129500000414_ref007","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0960129500000414_ref001","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"S0960129500000414_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T23:49:45Z","timestamp":1557877785000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000414\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,6]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,6]]}},"alternative-id":["S0960129500000414"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000414","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,6]]}}}