We propose a concurrent process calculus, called Calcul
Parallèle Logique (CPL), based on
the paradigm of computation as proof net construction in linear logic.
CPL uses a fragment
of first-order intuitionistic linear logic where formulas represent processes
and proof nets
represent successful computations. In these computations, communication
is expressed in an
asynchronous way by means of axiom links. We define testing equivalences
for processes,
which are based on a concept of interface, and use the power of proof theory
in linear logic.
Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis
