Relating Reasoning Methodologies in Linear Logic and Process Algebra

Yuxin Deng
(Carnegie Mellon University and Shanghai Jiao Tong University)
Iliano Cervesato
(Carnegie Mellon University)
Robert J. Simmons
(Carnegie Mellon University)

We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like 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 a labeled transition system and a coinductively defined simulation relation. This result establishes a connection between an approach to reason about process specifications and a method to reason about logic specifications.

In Sandra Alves and Ian Mackie: Proceedings 2nd International Workshop on Linearity (LINEARITY 2012), Tallinn, Estonia, 1 April 2012, Electronic Proceedings in Theoretical Computer Science 101, pp. 50–60.
Published: 15th November 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: