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

Recommendations

• Indexed and fibered structures for partial and total correctness assertions
• Fibred and Indexed Categories for Abstract Model Theory
• scientific article; zbMATH DE number 29052
• Indexed categories and bottom-up semantics of logic programs
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

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

• Dafny: An Automatic Program Verifier for Functional Correctness
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Title not available (Why is that?)
• Institutions: abstract model theory for specification and programming
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Title not available (Why is that?)
• 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 (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Weakest preconditions in fibrations
• Indexed and fibered structures for partial and total correctness assertions

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)