dc.contributor.author | Wolter, Uwe Egbert | |
dc.contributor.author | Martini, Alfio | |
dc.contributor.author | Haeusler, Edward Hermann | |
dc.date.accessioned | 2021-06-28T11:06:24Z | |
dc.date.available | 2021-06-28T11:06:24Z | |
dc.date.created | 2021-01-29T23:37:43Z | |
dc.date.issued | 2020 | |
dc.Published | Electronical Notes in Theoretical Computer Science. 2020, 348 125-145. | |
dc.identifier.issn | 1571-0661 | |
dc.identifier.uri | https://hdl.handle.net/11250/2761610 | |
dc.description.abstract | Indexed and fibred categorical concepts are widely used in computer science as models of logical systems and type theories. Here we focus on Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed category and fibred category theory. The structural features of the language are presented in an indexed setting, while the logical features of deduction are modeled in the fibred one. Especially, Hoare triples arise naturally as special arrows in a fibred category over a syntactic category of programs, while deduction in the Hoare calculus can be characterized categorically by the heuristic deduction = generation of cartesian arrows + composition of arrows. | en_US |
dc.language.iso | eng | en_US |
dc.publisher | Elsevier | en_US |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internasjonal | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/deed.no | * |
dc.title | Indexed and Fibred Structures for Hoare Logic | en_US |
dc.type | Journal article | en_US |
dc.type | Peer reviewed | en_US |
dc.description.version | publishedVersion | en_US |
dc.rights.holder | Copyright 2020 The Authors | en_US |
cristin.ispublished | true | |
cristin.fulltext | original | |
cristin.qualitycode | 1 | |
dc.identifier.doi | https://doi.org/10.1016/j.entcs.2020.02.008 | |
dc.identifier.cristin | 1883078 | |
dc.source.journal | Electronical Notes in Theoretical Computer Science | en_US |
dc.source.40 | 348 | |
dc.source.pagenumber | 125-145 | en_US |
dc.identifier.citation | Electronical Notes in Theoretical Computer Science. 2020, 348, 125-145 | en_US |
dc.source.volume | 348 | en_US |