Machine-checked model in Rocq establishes that governance is coterminous with expressibility via four primitive constructors in a symmetric monoidal category with capability bounds and verified coherence.
SCInfer: Refinement- Based Verification of Software Countermeasures Against Side- Channel Attacks
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
unclear 1representative citing papers
Mechanizes three governance theorems in Coq and proves two on paper for structural governance in AI systems, with runtime verification via property-based testing showing zero discrepancies.
Links noninterference to conditional independence so that probing security of masked algorithms can be checked inside the Lilac probabilistic separation logic.
citing papers explorer
-
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
Machine-checked model in Rocq establishes that governance is coterminous with expressibility via four primitive constructors in a symmetric monoidal category with capability bounds and verified coherence.
-
Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
Mechanizes three governance theorems in Coq and proves two on paper for structural governance in AI systems, with runtime verification via property-based testing showing zero discrepancies.
-
Formal Verification of Probing Security via Conditional Independence
Links noninterference to conditional independence so that probing security of masked algorithms can be checked inside the Lilac probabilistic separation logic.