Relating Reasoning Methodologies in Linear Logic and Process Algebra

TL;DR

This paper establishes a formal connection between reasoning methods in linear logic and process algebra, demonstrating their equivalence in a specific calculus through proof-theoretic and process-theoretic concepts.

Contribution

It shows that logical preorder and contextual preorder coincide in a CCS-like calculus derived from linear logic, linking logic and process algebra reasoning.

Findings

Proof-theoretic and process-theoretic notions coincide in the calculus.

Establishes a formal link between logic and process algebra reasoning.

Uses standard process algebra notions like labeled transition systems and simulation relations.

Abstract

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.