Computer Science Department
School of Computer Science, Carnegie Mellon University


Relating Reasoning Methodologies in
Linear Logic and Process Algebra

Yuxin Deng, Robert J. Simmons, Iliano Cervesato

December 2011


Also appears as Carnegie Mellon Qatar Campus
Technical Report CMU-CS-QTR-111.pdf

Keywords: Linear logic, process algebra, meta-reasoning, logical preorder, contextual preorder, simulation, labeled transition systems, equivalence, induction, coinduction

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.

44 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by