The Update Calculus
Abstract:
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