Target Language
Asynchronous variant of Milner”Ēs ?-calculus
new x in P (channel creation)
x![y] (output)
x?[y].P (input)
P | Q (parallel execution)
def x[y]=P in Q (process definition)
if x then P else Q (conditional branch)
x?[y].P | x![z] ? P{z/y}
def x[y]=P in x![z] ? def x[y]=P in P{z/y}
Previous slide
Next slide
Back to first slide
View graphic version