Abstract
A bigraphical reactive system (BRS) involves bigraphs, in which the nesting of nodes represents locality, independently of the edges connecting them. BRSs represent a wide variety of calculi for mobility, including λ-calculus and ambient calculus. A labelled transition system (LTS) for each BRS is here derived uniformly, adapting previous work of Leifer and Milner, so that under certain conditions the resulting bisimilarity is automatically a congruence. For an asynchronous λ-calculus, this LTS and its bisimilarity agree closely with the standard.
Original language | English |
---|---|
Title of host publication | POPL '03 Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages |
Publisher | ACM |
Pages | 38-49 |
Number of pages | 12 |
ISBN (Print) | 1-58113-628-5 |
DOIs | |
Publication status | Published - 2003 |