{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,24]],"date-time":"2025-07-24T11:01:05Z","timestamp":1753354865666,"version":"3.40.5"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2022,9,19]],"date-time":"2022-09-19T00:00:00Z","timestamp":1663545600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on partial and total correctness assertions within the framework of Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed and fibered category theory. We consider Hoare formulas with local, finite contexts, of program and logical variables. The structural features of Hoare assertions are presented in an indexed setting, while the logical features of deduction are modeled in the fibered one.<\/jats:p>","DOI":"10.1017\/s0960129522000275","type":"journal-article","created":{"date-parts":[[2022,9,19]],"date-time":"2022-09-19T09:28:05Z","timestamp":1663579685000},"page":"1145-1175","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["Indexed and fibered structures for partial and total correctness assertions"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7553-9858","authenticated-orcid":false,"given":"U.E.","family":"Wolter","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3704-6208","authenticated-orcid":false,"given":"A.R.","family":"Martini","sequence":"additional","affiliation":[]},{"given":"E.H.","family":"H\u00e4usler","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2022,9,19]]},"reference":[{"volume-title":"Institution-Independent Model Theory","year":"2008","author":"Diaconescu","key":"S0960129522000275_ref7"},{"key":"S0960129522000275_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6_17"},{"key":"S0960129522000275_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"S0960129522000275_ref17","doi-asserted-by":"crossref","unstructured":"Loeckx, J. and Sieber, K. (1987). The Foundations of Program Verification, 2nd ed., Stuttgart, Wiley-Teubner.","DOI":"10.1007\/978-3-322-96753-4"},{"key":"S0960129522000275_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_33"},{"key":"S0960129522000275_ref24","first-page":"39","volume-title":"Handbook of Logic in Computer Science","volume":"5.","author":"Pitts","year":"2000"},{"key":"S0960129522000275_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"S0960129522000275_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275"},{"key":"S0960129522000275_ref22","article-title":"Programming Language Foundations","volume":"2","author":"Pierce","year":"2018","journal-title":"Software Foundations Series"},{"key":"S0960129522000275_ref23","article-title":"Logical Foundations","volume":"1","author":"Pierce","year":"2018","journal-title":"Software Foundations Series"},{"key":"S0960129522000275_ref25","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs038"},{"key":"S0960129522000275_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.02.008"},{"key":"S0960129522000275_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"S0960129522000275_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000414"},{"key":"S0960129522000275_ref20","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzm045"},{"key":"S0960129522000275_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"S0960129522000275_ref5","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"S0960129522000275_ref19","doi-asserted-by":"publisher","DOI":"10.22456\/2175-2745.98483"},{"key":"S0960129522000275_ref14","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"141","author":"Jacobs","year":"2001"},{"key":"S0960129522000275_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"volume-title":"Texts in Computer Science","year":"2009","author":"Apt","key":"S0960129522000275_ref2"},{"key":"S0960129522000275_ref21","first-page":"436","volume-title":"COMPASS\/ADT","volume":"1130","author":"Pawlowski","year":"1995"},{"key":"S0960129522000275_ref11","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"S0960129522000275_ref12","first-page":"2","article-title":"Generic weakest precondition semantics from monads enriched with order","volume":"604","author":"Hasuo","year":"2015","journal-title":"Coalgebraic Methods in Computer Science."},{"volume-title":"Categories for Types","year":"1993","author":"Crole","key":"S0960129522000275_ref6"},{"volume-title":"Series in Computer Science","year":"1990","author":"Barr","key":"S0960129522000275_ref3"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,29]],"date-time":"2023-03-29T02:33:42Z","timestamp":1680057222000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000275\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,19]]},"references-count":26,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["S0960129522000275"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000275","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,9,19]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}