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.
Lecture Notes in Computer Science92
7 Pith papers cite this work. Polarity classification is still indexing.
7
Pith papers citing it
verdicts
UNVERDICTED 7representative citing papers
lqCCS provides scheduled semantics for quantum processes using physically admissible schedulers, yielding a bisimilarity that is adequate for indistinguishable quantum mixtures and a congruence for parallel composition.
Single-exponential algorithm for simple grammar bisimilarity yields first polynomial-time equivalence check for context-free session types via linear-valuation conversion.
Generalizes PDL to OPDL by distinguishing programs from traces via arbitrary operational semantics and proves cut-elimination for a non-wellfounded sequent calculus.
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.
Well-chosen transformations reduce LNT code for the Algorand consensus model by a factor of three while improving readability, with properties verified via visual checking, equivalence checking, and model checking.
This paper compiles and discusses several open problems in the modal logic for gossip protocols that use epistemic formulas.
citing papers explorer
-
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.
-
Verification of Quantum Protocols Adopting Physically Admissible Schedulers
lqCCS provides scheduled semantics for quantum processes using physically admissible schedulers, yielding a bisimilarity that is adequate for indistinguishable quantum mixtures and a congruence for parallel composition.
-
Simple grammar bisimilarity, with an application to session type equivalence
Single-exponential algorithm for simple grammar bisimilarity yields first polynomial-time equivalence check for context-free session types via linear-valuation conversion.
-
On Propositional Dynamic Logic and Concurrency
Generalizes PDL to OPDL by distinguishing programs from traces via arbitrary operational semantics and proves cut-elimination for a non-wellfounded sequent calculus.
-
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.
-
Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol
Well-chosen transformations reduce LNT code for the Algorand consensus model by a factor of three while improving readability, with properties verified via visual checking, equivalence checking, and model checking.
-
Open Problems in a Logic of Gossips
This paper compiles and discusses several open problems in the modal logic for gossip protocols that use epistemic formulas.