The Update Calculus

Joachim Parrow and Björn Victor


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.

Extended abstract: In M. Johnson, ed, Proceedings of AMAST'97, Sydney, volume 1349 of LNCS, pages 409-423. Springer-Verlag, 1997. (Postscript, compressed)
Full version: DoCS Technical report 97/93, September 1997 (Postscript, compressed)

See also the fusion calculus, which develops the update calculus to polyadic communication.

BibTeX entry:

@InProceedings{	  parrow.victor:update-calculus,
  author	= "Joachim Parrow and Bj{\"o}rn Victor",
  title		= "The Update Calculus",
  volume	= 1349,
  series	= "LNCS",
  booktitle	= "Proceedings of AMAST'97",
  editor	= "Michael Johnson",
  pages		= "409-423",
  year		= 1997,
  publisher	= "Springer",
  note		= "Full version available as Technical report DoCS
		   97/93, Uppsala University"

Björn Victor
Last modified: Tue Aug 25 11:04:47 1998 MET DST