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