Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
Sufficient incorrectness logic: SIL and separation SIL
4 Pith papers cite this work, alongside 4 external citations. Polarity classification is still indexing.
4
Pith papers citing it
4
external citations · external index
citation-role summary
background 1
citation-polarity summary
verdicts
UNVERDICTED 4roles
background 1polarities
background 1representative citing papers
Establishes a complete axiomatization for probabilistic Boolean circuits via Markov kernel semantics, using intermediate completeness theorems for partial Boolean circuits and probabilistic Boolean tapes in rig categories.
Kleene-Cartesian rig categories equip tape diagrams to handle imperative programs and program logic.
Unifies four axiomatic program logics and reduces simulation relations in refinement proofs to triple validity checks in those logics.
citing papers explorer
-
Hyper Separation Logic (extended version)
Hyper Separation Logic extends separation logic and Hyper Hoare Logic with a hyper separating conjunction to support arbitrary quantifier alternation for hyperproperties over heap programs, with a soundness proof in Isabelle/HOL.
-
Completeness for Probabilistic Boolean Tapes
Establishes a complete axiomatization for probabilistic Boolean circuits via Markov kernel semantics, using intermediate completeness theorems for partial Boolean circuits and probabilistic Boolean tapes in rig categories.
-
A Diagrammatic Basis for Computer Programming
Kleene-Cartesian rig categories equip tape diagrams to handle imperative programs and program logic.
-
Combining Axiomatic Models for Refinement Proofs
Unifies four axiomatic program logics and reduces simulation relations in refinement proofs to triple validity checks in those logics.