Abstract
We study the use of the π-calculus for semantical descriptions of languages such as Concurrent Idealised ALGOL (CIA), combining imperative, functional and concurrent features. We first present an operational semantics for CIA, given by SOS rules and a contextual form of behavioural equivalence; then a π-calculus semantics. As behavioural equivalence on π-calculus processes we choose the standard (weak early) bisimilarity. We compare the two semantics, demonstrating that there is a close operational correspondence between them and that the π-calculus semantics is sound. This allows for applying the π-calculus theory in proving behavioural properties of CIA phrases. We discuss laws and examples which have served as benchmarks to various semantics, and a more complex example involving procedures of higher order.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Arun-Kumar and M. Hennessy. An efficiency preorder for processes. Acta Informatica, 29:737–760, 1992.
S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electronic Notes in Theoretical Computer Science, 3, 1996.
S. Abramsky and G. McCusker. Full abstraction for idealized algol with passive expressions. Submitted for Publication, 1997.
S. Brookes. The essence of parallel algol. In Proc. LICS’96. IEEE, 1996. App. in vol. 2 of [OT97].
M. Boreale and D. Sangiorgi. Bisimulation in name-passing calculi without matching. In thirteen LICS Conf. IEEE Computer Society Press, 1998.
W. Ferreira, M. Hennessy, and A. Jeffrey. A theory of weak bisimulation for core CML. Technical report, School of Cognitive and Computing Sciences, University of Sussex, 1995.
M. Fiore, E. Moggi, and D. Sangiorgi. A fully-abstract model for the π-calculus. In 11th LICS. IEEE Computer Society Press, 1996.
K. Honda. Composing processes. In Proc. 23rd POPL. ACM Press, 1996.
D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2):103–112, 1996.
C. B. Jones. A π-calculus semantics for an object-based design notation. In E. Best, editor, Proc. CONCUR’ 93, volume 715 of LNCS, pages 158–172. Springer Verlag, 1993.
N. Kobayashi. A partially deadlock-free typed process calculus. In Proc. 12th LICS Conf. IEEE Computer Society Press., 1997.
N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the π-calculus. In Proc. 23rd POPL. ACM Press, 1996.
J. Kleist and D. Sangiorgi. Imperative objects and mobile processes. In Proc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET’98). North-Holland, 1998.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, LFCS, 1991.
R. Milner. Functions as processes. J. of Math. Struct. in Computer Science, 17:119–141, 1992.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Report ECS-LFCS-89-85,86, Dept. of Computer Science, University of Edinburgh, 1989. Two volumes, also appeared in Information and Computation 100:1–77,1992.
A. R. Meyer and K. Sieber. Towards fully abstract semantics for local variables: preliminary report. In Proc. 15th POPL, 1988. Also appeared in vol. 2 of [OT97].
R. Milner and D. Sangiorgi. The problem of weak bisimulation up-to. In Proc. CONCUR’92, volume 630 of LNCS. Springer, 1992.
I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Technical report, University of Stanford, 1990.
I. A. Mason and C. L. Talcott. References, local variables and operational reasoning. Technical report, University of Stanford, 1990.
[OT95] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658–709, 1995. Also appeared in [OT97].
P. W. O’Hearn and R. D. Tennent, editors. ALGOL-like Languages. Progress in Theoretical Computer Science. Birkhäuser, 1997. Two volumes.
A. M. Pitts. Reasoning about local variables with operationally-based logical relations. In Proc. LICS’96. IEEE, 1996. Also appeared in vol. 2 of [OT97].
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proc. LICS’93. IEEE, 1993. Also appeared in Mathematical Structures in Computer Science 6:5(1996) pp. 409–453.
J. C. Reynolds. The essence of ALGOL. In Algorithmic Languages, pages 345–372. North-Holland, 1981. Also appeared in vol. 1 of [OT97].
D. Sangiorgi. Lazy functions and mobile processes. Technical Report RR-2515, INRIA-Sophia Antipolis, 1995. To appear in “Festschrift volume in honor of Robin Milner’s 60th birthday”, MIT Press.
Davide Sangiorgi. On the proof method for bisimulation (extended abstract). In Proc. MFCS’95, volume 969 of LNCS, pages 479–488. Springer Verlag, 1995. Full version available electronically.
Ian Stark. A fully abstract domain model for the π-calculus. In Proc. LICS’96, pages 36–42. IEEE Computer Society Press, 1996.
D. Walker. Objects in the π-calculus. Information and Computation, 116:253–271, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Röckl, C., Sangiorgi, D. (1999). A π-calculus Process Semantics of Concurrent Idealised ALGOL. In: Thomas, W. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1999. Lecture Notes in Computer Science, vol 1578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49019-1_21
Download citation
DOI: https://doi.org/10.1007/3-540-49019-1_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65719-4
Online ISBN: 978-3-540-49019-7
eBook Packages: Springer Book Archive