Abstract
We show that adequate semantics can be provided for imperative higher order concurrent languages simply using syntactical final coalgebras. In particular we investigate and compare various behavioural equivalences on higher order processes defined by finality using hypersets and c.m.s. 's. Correspondingly, we derive various coinduction and mixed induction-coinduction proof principles for establishing these equivalences.
Work supported by CNR, EEC Science grant MASK, and MURST 40% grant.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P.Aczel, Non-wellfounded sets, Number 14, Lecture Notes CSLI, 1988.
J.de Bakker, F.van Breugel, Topological models for higher order control flow, MFPS'93 Conference Proc., Brookes et al. eds., Springer LNCS Vol.802, 1993.
J.de Bakker, F.van Breugel, Metric Semantics for Second Order Communication, Technical Report, McGill University, Montreal, July 1995.
M.Barr, Terminal coalgebras in well-founded set theory, TCS, 114:299–315, 1993.
Barwise, Hypersets, The Mathematical Intelligencer, Vol.13(4):31–41, 1991.
M.Forti, F.Honsell, Set Theory with Free Construction Principles, Annali Scuola Normale Sup. Pisa, Cl. Sci., (IV), 10:493–522, 1983.
M.Forti, F.Honsell, M.Lenisa, Processes and Hyperuniverses, MFCS'94 Conference Proceedings, I.Privara et al. eds., Springer LNCS Vol.841:352–363, Košice, 1994.
P.Freyd, Algebraically complete categories, A.Carboni et al. eds, Category Theory '90 Springer LNM, Vol.1144:95–104, Como, 1992.
J.F.Groote, F.Vaandrager, Structured Operational Semantics and Bisimulation as a Congruence, Information and Computation Vol.100:202–260, 1992.
F.Honsell, M.Lenisa, Final Semantics for untyped λ-calculus, M.Dezani et al. eds, TLCA'95 Springer LNCS Vol.902:249–265, Edinburgh, 1995.
A.M.Pitts, Relational Properties of Recursively Defined Domains, 8th LICS Conference Proceedings, IEEE Computer Society Press:86–97, 1993.
J.J.M.M.Rutten, Processes as terms: non-wellfounded models for bisimulation, Math.Struct.Comp.Sci., Vol.2(3):257–275, 1992.
J.J.M.M.Rutten, D.Turi, On the Foundations of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders, REX Conference Proceedings, J.deBakker et al. eds., Springer LNCS Vol.666:477–530, 1993.
J.J.M.M.Rutten, D.Turi, Initial algebra and final coalgebra semantics for concurrency, Report CS-R9409, CWI, Amsterdam, January 1994.
D.Sangiorgi, Expressing Mobility in Process Algebras: First-Oder and Higher-Order Paradigms, Ph.D thesis CST-99-93, University of Edinburgh, 1992.
B.Thomsen, A Calculus of Higher Order Communicating Systems, Proc. 16th Annual ACM Symp. on Principles of Programming Languages:143–154, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lenisa, M. (1996). Final semantics for a higher order concurrent language. In: Kirchner, H. (eds) Trees in Algebra and Programming — CAAP '96. CAAP 1996. Lecture Notes in Computer Science, vol 1059. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61064-2_32
Download citation
DOI: https://doi.org/10.1007/3-540-61064-2_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61064-9
Online ISBN: 978-3-540-49944-2
eBook Packages: Springer Book Archive