Encoding pi calculus in Calculus of Structures

Hi,
I recently had a discussion with Alessio about the problem of
encoding pi calculus in first-order BV. It can be seen as an extension
of Paola's work on encoding CCS in BV. This is meant to be a possible
research topic in CoS. Comments and suggestions are welcome.

Best regards,
-Alwen

---
The general motivation is to answer the question:
can we give a logical (proof theoretical) interpretation to  a process 
calculus?
There are at least three approaches to this problem: the process-as-proof
approach, process-as-formula approach, and process-as-term.
The last approach typically encodes processes using terms in logic and then
define the operational semantics of the transition system of the process 
calculus as a theory
in logic (which is usually in the form of Horn clauses).
I will take the second approach in the following discussion.
In this approach, we encode process constructors as logical
connectives (or structural relations, in CoS) and we are interested in 
finding a suitable
logical notion that correspond to reduction in process calculi.
More specifically, I am interested in name-passing calculi,
pi-calculus in this case, and in the following correspondences
(I shall identify process with formula)
(a) Given two processes P and Q, P  -->* Q (P reduces to Q, modulo
   some structural congruence) if and only if
   Q --o P (Q linearly implies P)
(b) Given two process P and Q, P  -->* Q if and only if
   we can derive P from Q in a certain cut free fragment of logic

The correspondence (a) is of course stronger than (b), and it might
be more difficult to get. One problem, for example, is in encoding
the restriction operator, nu, in pi-calculus. A standard approach is to use
universal quantifier to encode restriction. Given the encoding of
parallel composition as par, we have the following implication (I use
CoS notation to write par as [ , ] )

 [forall x Px, forall x Qx] --o forall x [Px, Qx]

Now the problem is that the processes (nu x Px | nu x Q x) and
nu x (Px | Qx) are not related by reduction nor by structural congruence.
A more serious problem is what I call the diagonal problem:
in logic we have
 forall x forall y Pxy --o forall z P zz,
but in pi-calculus, nu x nu y P xy is not related by reduction (and 
should not be,
by the definition of the nu operator) to the process nu z Pzz.
Hence this approach seems to require a "new" quantifier.

The problems mentioned above do not arise in (b), provided we restrict to
a certain fragment of logic (e.g., the down fragment of
systems in CoS) and hence this could be the right
approach to start with. Of course the fragment should be a natural
one and not too restrictive. A good starting point for this approach
would be to look at Paola Bruscoli's work on encoding CCS in BV.
In our case, we would have to extend BV with quantifiers, which
should be obvious (see Kai Bruennler's thesis for the treatment of 
quantifiers
in CoS) and encode bound input prefix as follows:

       a(x).Px is encoded as  exists x. <ax; Px>

The down-rule for the quantifiers are

S{forall x [R, T] }
------------------------------ u_
S[forall x R, exists x T]

     S{P t}
-------------------- n_
S{exists x P x}

This approach could be a straightforward extension of  Paola's work
from CCS to pi-calculus. There might be some subtlety involving bound input
prefix, e.g., in Paola's terminology, we would have to restrict the 
application
of n_ to the "right-context". But one can start first with pi calculus 
with free input prefix.