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.
Title resolution pending
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
roles
background 2polarities
background 2representative citing papers
Foxtrot is the first higher-order separation logic for contextual refinement of higher-order concurrent probabilistic programs with higher-order local state, mechanized in Rocq and Iris.
Evidence-tracked tape semantics yields a higher-order logic for randomized programs in which entailments are witnessed by uniform evidence transformers and quantitative probabilities arise by interpretation under a chosen tape measure.
A type system with types over normal forms and a decidable complement operator via subtyping is sound and complete, deriving refutation principles to certify incorrectness in functional programs.
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.
-
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Foxtrot is the first higher-order separation logic for contextual refinement of higher-order concurrent probabilistic programs with higher-order local state, mechanized in Rocq and Iris.
-
Evidence-Tracked Tape Semantics for Probabilistic Computation
Evidence-tracked tape semantics yields a higher-order logic for randomized programs in which entailments are witnessed by uniform evidence transformers and quantitative probabilities arise by interpretation under a chosen tape measure.
-
A Complementary Approach to Incorrectness Typing
A type system with types over normal forms and a decidable complement operator via subtyping is sound and complete, deriving refutation principles to certify incorrectness in functional programs.