Syntax for BoCa
Preterms are defined by the following grammar:
where "a" ranges over a denumerable set of names, k is any
integer ≤0.
The type syntax is defined by the following productions:
where
and Φ is generated by closing under functional composition
the following set of functions:
Term and type syntax translate into Prolog terms as follows (by respecting the same ordering of clauses as in the above definitions):
Processes 
P 
::= _  zero  Pi pref P  PP  spamb(M, K, P) where "spamb" stands for space ambient  bang (Pi, P)  nu(A : W, P) 
Capabilities 
C 
::= in(M)  out(M)  open(M)  open_bar  get(M)  get_up  put  put_down 
Message 
M 
::= A  C  M dot M 
Prefix 
Pi 
::= M  sp(K) 

K 
::= positive integer 

A 
::= alphanumeric string beginnig by 'a' (ambient names) 


Type syntax 

T 
::= proc(EXP,EXP) 

W 
::= amb(Iota)  cap(Phi) 

Phi 
::= id  put  get  open(EXP,EXP)  comp(Phi,Phi) 

EXP 
::= d(A)  i(A)  Z  EXP + EXP  EXP  EXP  min_(EXP, EXP)  max_(EXP,EXP) 

Z 
::= any integer 

Iota 
::= sqb(N1,N2) where 0 =< N1 =< N2 are integers 


To run the program one is expected to write: boca(G,P,T,D) where 

G 
is the environment 

P 
is the process 

T 
is the type 

D 
is the set of conditions that must be satisfied in order to type the process P 
