Indexed and fibred structures for Hoare logic

DOI10.1016/j.entcs.2020.02.008zbMath1495.03053OpenAlexW3013738153WikidataQ113317339 ScholiaQ113317339MaRDI QIDQ2219084

A. R. Martini, U. E. Wolter, Edward Hermann Haeusler

Publication date: 19 January 2021

Full work available at URL: https://doi.org/10.1016/j.entcs.2020.02.008

zbMATH Keywords

Grothendieck constructionfibrationsHoare logicindexed categoriesweakest liberal preconditioninstitution

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (1)

Weakest preconditions in fibrations

Uses Software

• Dafny

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dafny: An Automatic Program Verifier for Functional Correctness
• Categories for Software Engineering
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• Institutions: abstract model theory for specification and programming
• One Logic to Use Them All
• Fibred and Indexed Categories for Abstract Model Theory
• An axiomatic basis for computer programming

This page was built for publication: Indexed and fibred structures for Hoare logic