Relating Reasoning Methodologies in Linear Logic and Process Algebra
Yuxin Deng, Robert J. Simmons, and Iliano Cervesato
We show that the proof-theoretic notion of logical preorder coincides
with the process-theoretic notion of contextual 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 contextual preorder, and a method to reason
about logic specifications, the logical preorder.