Abstract
A fully abstract denotational semantics for the higher-order process language HOPLA is presented. It characterises contextual and logical equivalence, the latter linking up with simulation. The semantics is a clean, domain-theoretic description of processes as downwards-closed sets of computation paths: the operations of HOPLA arise as syntactic encodings of canonical constructions on such sets; full abstraction is a direct consequence of expressiveness with respect to computation paths; and simple proofs of soundness and adequacy shows correspondence between the denotational and operational semantics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benton, P.N.: A mixed linear and non-linear logic: proofs, terms and models (extended abstract). In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933. Springer, Heidelberg (1995)
Bräuner, T.: An Axiomatic Approach to Adequacy. Ph.D. Dissertation, University of Aarhus, BRICS Dissertation Series DS-96-4 (1996)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: modal logics for mobile ambients. In: Proc. POPL 2000 (2000)
Cattani, G.L., Winskel, G.: Profunctors, open maps and bisimulation. Manuscript (2000)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)
Gordon, A.D.: Bisimilarity as a theory of functional programming. In: Proc. MFPS 1995. ENTCS 1 (1995)
Hennessy, M.C.B., Plotkin, G.D.: Full abstraction for a simple parallel programming language. In: Becvar, J. (ed.) MFCS 1979. LNCS, vol. 74. Springer, Heidelberg (1979)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985)
Hennessy, M.: A fully abstract denotational model for higher-order processes. Information and Computation 112(1), 55–95 (1994)
Hoare, C.A.R.: A Model for Communicating Sequential Processes. Technical monograph, PRG-22, University of Oxford Computing Laboratory (1981)
Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127, 164–185 (1996)
Larsen, K.G., Winskel, G.: Using information systems to solve recursive domain equations effectively. In: Plotkin, G., MacQueen, D.B., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173. Springer, Heidelberg (1984)
Melliès, P.-A.: Categorical models of linear logic revisited. Theoretical Computer Science (2002) (submitted to)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Information and Computation 100(1), 1–77 (1992)
Morris, J.H.: Lambda-Calculus Models of Programming Languages. PhD thesis, MIT (1968)
Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1), 85–108 (1981)
Nygaard, M.: Towards an operational understanding of presheaf models. Progress report, University of Aarhus (2001)
Nygaard, M., Winskel, G.: Linearity in process languages. In: Proc. LICS 2002 (2002)
Nygaard, M., Winskel, G.: HOPLA—a higher-order process language. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 434. Springer, Heidelberg (2002)
Nygaard, M., Winskel, G.: Domain theory for concurrency. Theoretical Computer Science (2003) (submitted to)
Scott, D.S.: Domains for denotational semantics. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140. Springer, Heidelberg (1982)
Seely, R.A.G.: Linear logic, ∗-autonomous categories and cofree coalgebras. In: Proc. Categories in Computer Science and Logic (1987)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Winskel, G.: A presheaf semantics of value-passing processes. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)
Winskel, G., Zappa Nardelli, F.: Manuscript (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nygaard, M., Winskel, G. (2003). Full Abstraction for HOPLA. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive