Syntax for BoCa

Pre-terms 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:


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 | P|P | 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


Comments to: falzetta[at]di[dot]unito[dot]it Last update: February, 2005