Indexed and Fibred Structures for Hoare Logic
Journal article, Peer reviewed
Published version

Åpne
Permanent lenke
https://hdl.handle.net/11250/2761610Utgivelsesdato
2020Metadata
Vis full innførselSamlinger
- Department of Informatics [1002]
- Registrations from Cristin [11365]
Originalversjon
Electronical Notes in Theoretical Computer Science. 2020, 348, 125-145 https://doi.org/10.1016/j.entcs.2020.02.008Sammendrag
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.