Indexed and Fibred Structures for Hoare Logic
Journal article, Peer reviewed
Published version
![Thumbnail](/bora-xmlui/bitstream/handle/11250/2761610/2020_LSFA19_Indexed-and-fibred-Hoare-logic.pdf.jpg?sequence=6&isAllowed=y)
View/ Open
Date
2020Metadata
Show full item recordCollections
- Department of Informatics [978]
- Registrations from Cristin [10237]
Original version
Electronical Notes in Theoretical Computer Science. 2020, 348, 125-145 https://doi.org/10.1016/j.entcs.2020.02.008Abstract
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.