Relating Reasoning Methodologies in Linear Logic and Process Algebra
Yuxin Deng, Rob J. Simmons, and Iliano Cervesato
We show that the proof-theoretic notion of logical preorder coincides with
the process-theoretic notion of barbed preorder for a CCS-like process calculus
obtained from the formula-as-process interpretation of a fragment of linear logic.
The argument makes use of other standard notions in process algebra, namely
simulation and labeled transition systems. This result establishes a connection
between an approach to reason about process specifications, the barbed preorder,
and a method to reason about logic specifications, the logical preorder.