The paper provides a 14K-line Rocq proof of safety and liveness for MPST via coinductive global/local types, operational correspondence, and mechanized projection/subtyping relations.
hub
36th Annual
22 Pith papers cite this work. Polarity classification is still indexing.
22
Pith papers citing it
hub tools
citation-role summary
background 4
citation-polarity summary
roles
background 4representative citing papers
Coverability for order-k nested reset counter systems is F_Ωk-complete.
Amaryllis is the first general-purpose probabilistic separation logic supporting dynamic memory allocation, independence, and conditioning, with a mechanized soundness proof in Rocq.
Star-height of Parikh images is bounded by 2 for one-register automata but the rational conjecture fails for multiple registers, showing Parikh's theorem does not hold over infinite alphabets.
APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
k-WL is incomplete on simple spectrum graphs; PRiSM is the first provably complete canonicalization for their eigendecompositions.
Proof nets are defined for PiL with a correctness criterion, sequentialization procedure, and translation algorithm, establishing a canonical representation of sequent calculus derivations modulo rule permutations.
Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
A differentiable neural model recovers ground-truth lifted action schemas from state traces by jointly learning schemas and inferring unobserved action arguments.
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.
Cocartesian fibrations are defined in synthetic simplicial type theory with closure properties proved using a novel equivalence between LARI adjunctions and initial sections.
Craig interpolants for hybrid modal logics are computable in 4-EXPTIME when they exist, while uniform interpolant existence is undecidable.
Semantic typing via coinductively defined interpretations on a typed operational semantics ensures information flow control and non-interference for TinySol contracts that use fallback functions.
Tabular modal logics admit propositionally sized interpolants and strongest implicates iff NP ⊆ P/poly, while non-tabular ones require exponential size unconditionally.
Logic-based Weisfeiler-Leman variants enable graph-to-table conversion for classification that matches GNN and graph transformer accuracy while running 5-20x faster without GPUs.
The paper reformulates polymorphisms in CSPs and PCSPs as right Kan extensions and supplies purely categorical proofs that complexity is determined by these structures.
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
Extends complexity dichotomy for monoid equation solving with promises to include arbitrary relations and finitely generated M.
Introduces an association relation for proving subject reduction in multiparty session π-calculus, guaranteeing session fidelity, deadlock freedom, and liveness from global types.
The pushout of entangled and parameterized quantum information in monoidal categories yields the external tensor product on flat K-theory bundles.
Logical families of stable and total profunctors are definable by MLL+MIX proof-nets.
citing papers explorer
-
Formally Verified Liveness with Multiparty Session Types in Rocq
The paper provides a 14K-line Rocq proof of safety and liveness for MPST via coinductive global/local types, operational correspondence, and mechanized projection/subtyping relations.
-
The Complexity of Nested Reset Counter Systems
Coverability for order-k nested reset counter systems is F_Ωk-complete.
-
First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
Amaryllis is the first general-purpose probabilistic separation logic supporting dynamic memory allocation, independence, and conditioning, with a mechanized soundness proof in Rocq.
-
Star Complexity of Parikh Images of Languages over Infinite Alphabets
Star-height of Parikh images is bounded by 2 for one-register automata but the rational conjecture fails for multiple registers, showing Parikh's theorem does not hold over infinite alphabets.
-
A Program Logic for Abstract (Hyper)Properties
APPL is a sound, relatively complete abstract program logic that subsumes Hoare, incorrectness, and hyperproperty logics via lattice semantics and a non-idempotent monoidal operator for nondeterminism.
-
Weisfeiler-Leman Is Incomplete on Simple Spectrum Graphs, so Canonicalize Them
k-WL is incomplete on simple spectrum graphs; PRiSM is the first provably complete canonicalization for their eigendecompositions.
-
Proof Nets for PiL (Full Version)
Proof nets are defined for PiL with a correctness criterion, sequentialization procedure, and translation algorithm, establishing a canonical representation of sequent calculus derivations modulo rule permutations.
-
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
-
Differentiable Learning of Lifted Action Schemas for Classical Planning
A differentiable neural model recovers ground-truth lifted action schemas from state traces by jointly learning schemas and inferring unobserved action arguments.
-
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.
-
Fibrations in Directed Type Theory
Cocartesian fibrations are defined in synthetic simplicial type theory with closure properties proved using a novel equivalence between LARI adjunctions and initial sections.
-
Computation and Size of Interpolants for Hybrid Modal Logics
Craig interpolants for hybrid modal logics are computable in 4-EXPTIME when they exist, while uniform interpolant existence is undecidable.
-
Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts
Semantic typing via coinductively defined interpretations on a typed operational semantics ensures information flow control and non-interference for TinySol contracts that use fallback functions.
-
The Size of Interpolants in Modal Logics
Tabular modal logics admit propositionally sized interpolants and strongest implicates iff NP ⊆ P/poly, while non-tabular ones require exponential size unconditionally.
-
Graph Learning via Logic-Based Weisfeiler-Leman Variants and Tabularization
Logic-based Weisfeiler-Leman variants enable graph-to-table conversion for classification that matches GNN and graph transformer accuracy while running 5-20x faster without GPUs.
-
A categorical perspective on constraint satisfaction: The wonderland of adjunctions
The paper reformulates polymorphisms in CSPs and PCSPs as right Kan extensions and supplies purely categorical proofs that complexity is determined by these structures.
-
Logical Relations for Session-Typed Concurrency
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
-
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
SAQR-QC is a new logic for scalable approximate quantitative reasoning about quantum circuits via local qubit operations and controlled precision loss, demonstrated on GHZ circuits and quantum phase estimation.
-
Equations over Finite Monoids with Infinite Promises
Extends complexity dichotomy for monoid equation solving with promises to include arbitrary relations and finitely generated M.
-
Less is More Revisited: Association with Global Protocols and Multiparty Sessions
Introduces an association relation for proving subject reduction in multiparty session π-calculus, guaranteeing session fidelity, deadlock freedom, and liveness from global types.
-
Entanglement of Sections: The pushout of entangled and parameterized quantum information
The pushout of entangled and parameterized quantum information in monoidal categories yields the external tensor product on flat K-theory bundles.
-
Full Definability in a Profunctorial Model
Logical families of stable and total profunctors are definable by MLL+MIX proof-nets.