UC, Categorically: Rigorous Diagrammatic Proofs

arXiv:2608.04521 · cs.LO, cs.CR, math.CT · Submitted 2026-08-05 · Read on arXiv

Pooya Farshim, Martti Karvonen, Andre Knispel, Markulf Kohlweiss, Philip Wadler

cs.LO, cs.CR, math.CT

Submitted: 2026-08-05

Project page: https://actconf2026.github.io/papers

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Composition — 71× in this paper · explained in 2 episodes
• Generator — 10× in this paper · explained in 2 episodes
• Universal Composability — 6× in this paper
• Axioms — 5× in this paper · explained in 2 episodes
• Verification — 3× in this paper · explained in 2 episodes
• Computer Security Foundations Symposium — 2× in this paper
• Core — 2× in this paper · explained in 2 episodes
• Generalization — 2× in this paper · explained in 14 episodes
• Coherence — 1× in this paper · explained in 2 episodes
• Compositionality — 1× in this paper · explained in 2 episodes
• Domain-Specific Language (DSL) — 1× in this paper · explained in 2 episodes
• Formal Verification — 1× in this paper · explained in 2 episodes
• GHZ State — 1× in this paper · explained in 3 episodes
• Information Leakage — 1× in this paper · explained in 2 episodes
• Papers — 1× in this paper · explained in 3 episodes
• Quantum Circuits — 1× in this paper · explained in 2 episodes
• UC to Robust Compilation — 1× in this paper
• ZX-calculus — 1× in this paper · explained in 2 episodes

Sources

• All graph state verification protocols are composably secure

Related papers

• Reasoning about Continuous-Variable Quantum Systems
• Formalizing Flag Algebras in Lean
• An Information-Flow Perspective on Explainability Requirements: Specification and Verification
• A programming language combining quantum and classical control
• Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
• Global Convergence of Detailed Balanced Mass Action Systems