Indexed and fibred structures for Hoare logic

DOI10.1016/J.ENTCS.2020.02.008zbMATH Open1495.03053OpenAlexW3013738153WikidataQ113317339 ScholiaQ113317339MaRDI QIDQ2219084FDOQ2219084

A. R. Martini, Edward Hermann Haeusler, Uwe Wolter

Publication date: 19 January 2021

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

zbMATH Keywords

fibrationsHoare logicGrothendieck constructionindexed 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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Dafny: An Automatic Program Verifier for Functional Correctness
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Institutions: abstract model theory for specification and programming
• An axiomatic basis for computer programming
• One Logic to Use Them All
• Categories for Software Engineering
• Fibred and Indexed Categories for Abstract Model Theory
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Weakest preconditions in fibrations

Uses Software

• Dafny

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2219084)