SuperDP refutes ε-DP via simultaneous synthesis of input pairs and witness functions using upper expectation supermartingales and lower expectation submartingales, delivering the first fully automated, sound, and semi-complete method applicable to both discrete and continuous stochastic mechanisms.
In: Proceedings of the 44th ACM SIGPLAN Sympo- sium on Principles of Programming Languages (POPL)
8 Pith papers cite this work. Polarity classification is still indexing.
8
Pith papers citing it
citation-role summary
background 2
citation-polarity summary
years
2026 8roles
background 2polarities
background 2representative citing papers
Programs emit intents checked against policies by a governed runtime before effects occur, with formal specification, Rocq verification of 454 theorems, and BEAM implementation.
General criteria for minimal models of streaming transducers are established, yielding effective minimization for variants of streaming string-to-tree transducers that build terms at leaves or roots.
Credit-based amortized analysis is sound for persistent data structures when credits are stored only on thunks, and Okasaki's debit approach receives a formal operational semantics.
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.
LBAC is a new programming model that enforces user-specified policies on agentic applications by requiring agent-generated programs to be well-typed in the context of the scaffolding code.
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
Introduces Packed Plan Forest (PPF) as a polynomially bounded structure that encodes feasible ambiguous logical plans while pruning infeasible ones in cross-model NL-to-DB query planning.
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.
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.