relating linear logic and the pi-calculus

To: types
Subject: relating linear logic and the pi-calculus
From: dale@saul.cis.upenn.edu (Dale Miller)
Date: Sat, 20 Jun 92 06:11:13 EDT
Sender: meyer@theory.lcs.mit.edu
Date: Wed, 17 Jun 92 09:53:22 EDT
To: linear@cs.stanford.edu

The following paper is available via anonymous ftp.

	   The $\pi$-calculus as a theory in linear logic:
			 Preliminary results

			     Dale Miller
		      University of Pennsylvania

The agent expressions of the $\pi$-calculus can be translated into a
theory of linear logic in such a way that the reflective and
transitive closure of $\pi$-calculus (unlabeled) reduction is
identified with ``entailed-by''.  Under this translation, parallel
composition is mapped to the multiplicative disjunct (``par'') and
restriction is mapped to universal quantification.  Prefixing,
non-deterministic choice ($+$), replication ($!$), and the match guard
are all represented using non-logical constants, which are specified
using a simple form of axiom, called here a {\em process clause}.
These process clauses resemble Horn clauses except that they may have
multiple conclusions; that is, their heads may be the par of atomic
formulas.  Such multiple conclusion clauses are used to axiomize
communications among agents.  Given this translation, it is nature to
ask to what extent proof theory can be used to understand the
meta-theory of the $\pi$-calculus.  We present some preliminary
results along this line for $\pi_0$, the ``propositional'' fragment of
the $\pi$-calculus, which lacks restriction and value passing ($\pi_0$
is a subset of CCS).  Using ideas from proof-theory, we introduce {\em
co-agent} and show that they can specify some testing equivalences for
$\pi_0$.  If negation-as-failure-to-prove is permitted as a co-agent
combinator, then testing equivalence based on co-agents yields
observational equivalence for $\pi_0$.  This latter result follows
>from observing that co-agents are isomorphic to formulas in the
Hennessy-Milner modal logic.

________________________________________________________________
This paper can be retrieved by anonymous ftp using the instructions
below.  If you want a copy but cannot use ftp to this site, send me
your postal address.

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/miller
ftp> binary
ftp> get pic.dvi.Z
ftp> quit

Use the unix uncompress command on this file to get pic.dvi.
Current reference for this paper is

@techreport(miller92tr,
  Author="Dale Miller",
  Title="The $\pi$-calculus as a theory in linear logic: Preliminary results",
  Month="June",
  Year=1992,
  Institution="Computer Science Department, University of Pennsylvania",
  number="MS-CIS-92-48",
  Note="Submitted.  Available using anonymous ftp from host
      ftp.cis.upenn.edu and the file pub/papers/miller/pic.dvi.Z.")