REVIEW 1 cited by
Proofs as Execution Trees for the {π}-Calculus
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Proofs as Execution Trees for the {π}-Calculus
read the original abstract
In this paper, we establish the foundations of a novel logical framework for the {\pi}-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent processes as formulas, and we interpret proofs as computations. For this purpose, we define a cut-free sequent calculus for an extension of first-order multiplicative and additive linear logic. This extension includes a non-commutative and non-associative connective to faithfully model the prefix operator, and nominal quantifiers to represent name restriction. Finally, we design proof nets providing canonical representatives of derivations up to local rule permutations.
Forward citations
Cited by 1 Pith paper
-
Causality in Pure Quantum Computation with Quantum Control
A typed lambda calculus based on intuitionistic BV logic blocks higher-order quantum-control programs that violate causality, and its categorical model excludes the OCB process.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.