Indexed and fibered structures for partial and total correctness assertions

DOI10.1017/S0960129522000275MaRDI QIDQ5889306

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

Publication date: 19 April 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

fibrationsHoare logicindexed categoriespartial correctness assertionstotal correctness assertions

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Dafny
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Verification of sequential and concurrent programs
• Weakest preconditions in fibrations
• Graded Hoare logic and its categorical semantics
• Institution-independent model theory
• Dafny: An Automatic Program Verifier for Functional Correctness
• Hoare Logic in the Abstract
• Guarded commands, nondeterminacy and formal derivation of programs
• Soundness and Completeness of an Axiom System for Program Verification
• Categories for Types
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic
• Institutions: abstract model theory for specification and programming
• Logic in Computer Science
• Towards a uniform presentation of logical systems by indexed categories and adjoint situations
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• Fibred and Indexed Categories for Abstract Model Theory

This page was built for publication: Indexed and fibered structures for partial and total correctness assertions