Indexed and fibred structures for Hoare logic

DOI10.1016/J.ENTCS.2020.02.008MaRDI QIDQ2219084zbMATH OpenOpenAlexWikidataFDO

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

Publication date 19 January 2021

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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)

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

Cites work

• scientific article; zbMATH DE number 3680046 (Why is no real title available?)
• scientific article; zbMATH DE number 46995 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• An axiomatic basis for computer programming
• Categories for Software Engineering
• Dafny: an automatic program verifier for functional correctness
• Fibred and Indexed Categories for Abstract Model Theory
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Institutions: abstract model theory for specification and programming
• One logic to use them all
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

Cited in

(5)

• scientific article; zbMATH DE number 5917724 (Why is no real title available?)
• scientific article; zbMATH DE number 500952 (Why is no real title available?)
• Weakest preconditions in fibrations
• Indexed and fibered structures for partial and total correctness assertions
• Indexed categories and bottom-up semantics of logic programs

Describes a project that uses

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)