CMU-CS-QTR-111
Computer Science Qatar
School of Computer Science, Carnegie Mellon University



CMU-CS-QTR-111

Relating Reasoning Methodologies in
Lienar Logic and Process Algebra

Yuxin Deng, Robert J. Simmons, Illiano Cervesato

December 2011

CMU-CS-QTR-111.pdf

Also appears as Computer Science Department
Technical Report CMU-CS-11-145.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 reports@cs.cmu.edu