[Prev][Next][Index][Thread]

Paper by Bellin & Scott





 A paper by Gianluigi Bellin and Philip Scott, entitled
"On the Pi Calculus and Linear Logic", is available by
anonymous ftp from Imperial College.

ftp to theory.doc.ic.ac.uk  , in the directory theory/papers/Scott .

The paper works out some connections between a version of Milner's
Pi-Calculus (a language for concurrent processes) and Abramsky's
proofs-as-processes generalization of Curry-Howard.  Here is the
official abstract.

\begin{abstract}
We detail  Abramsky's ``proofs-as-processes''
paradigm for interpreting classical linear logic (CLL)
into a  ``synchronous'' version of the $\pi$-calculus recently proposed
by Milner. The translation is given at the abstract level
of proof structures. We give a detailed treatment of information
flow in proof-nets and show how to mirror various evaluation strategies
for proof normalization. We also give Soundness and Completeness results
for the process-calculus translations of various fragments of CLL. The
paper also gives a self-contained introduction to some of the deeper
proof-theory of CLL, and its process interpretation.
\end{abstract}

                         Phil Scott  scpsg@acadvm1.uottawa.ca
                         Gianluigi Bellin  bellin@maths.oxford.ac.uk