The Update Calculus

摘要

In the update calculus concurrent processes can perform update actions with side effects, and a scoping operator can be used to control the extent of the update. in this way it incorporates fundamental concepts both from imperative languages or concurrent constraints formalisms, and from functional formalisms such as the #lambda#- and #pi#-calculi. Structurally it is similar to but simpler than the #pi#-calculus; it has only one binding operator and a symmetry between input and output. We define the structured operational semantics and the proper bisimulation equivalence and congruence, and give a complete axiomatization. The #pi#-calculus turns out to be an asymmetric subcalculus.