[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