A Linear Metalanguage for Concurrency

Forfattere

  • Glynn Winskel

DOI:

https://doi.org/10.7146/brics.v5i31.19437

Resumé

A metalanguage for concurrent process languages is introduced.
Within it a range of process languages can be defined, including
higher-order process languages where processes are passed and received as arguments. (The process language has, however, to be linear, in the sense that a process received as an argument can be run at most once, and not include name generation as in the Pi-Calculus.) The metalanguage is provided with two interpretations both of which can be understood as categorical models of a variant of linear logic. One interpretation is in a
simple category of nondeterministic domains; here a process will denote its set of traces. The other interpretation, obtained by direct analogy with the nondeterministic domains, is in a category of presheaf categories; the nondeterministic branching behaviour of a process is captured in its denotation as a presheaf. Every presheaf category possesses a notion of (open-map) bisimulation, preserved by terms of the metalanguage. The
conclusion summarises open problems and lines of future work.

Downloads

Publiceret

1998-06-01

Citation/Eksport

Winskel, G. (1998). A Linear Metalanguage for Concurrency. BRICS Report Series, 5(31). https://doi.org/10.7146/brics.v5i31.19437