Abstract
This paper investigates a methodology of using FM (Fraenkel-Mostowski) sets, and the ideas of nominal set theory, to adjoin name generation to a semantic theory. By developing a domain theory for concurrency within FM sets the domain theory inherits types and operations for name generation, essentially without disturbing its original higher-order features. The original domain theory had a metalanguage HOPLA (Higher Order Process Language) and accordingly this expands to a metalanguage, Nominal HOPLA, with name generation (closely related to an earlier language new-HOPLA). Nominal HOPLA possesses an operational and denotational semantics which are related via soundness and adequacy results, again carried out within FM sets.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Benton, N., Bierman, G., de Paiva, V., Hyland, M.: Linear lambda-calculus and categorical models revisited. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 61–84. Springer, Heidelberg (1993)
Gabbay, M.J.: A Theory of Inductive Definitions with Alpha-Equivalence. PhD thesis, Cambridge University (2001)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2001)
Nygaard, M., Winskel, G.: Domain theory for concurrency. Theor. Comput. Sci. 316(1-3), 153–190 (2004)
Turner, D.C.: Nominal Domain Theory for Concurrency. PhD thesis, Cambridge University (submitted) (2008), http://www.cl.cam.ac.uk/~dct25/
Winskel, G.: Name generation and linearity. In: LICS 2005: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, pp. 301–310. IEEE Computer Society Press, Los Alamitos (2005)
Winskel, G., Larsen, K.G.: Using information systems to solve recursive domain equations effectively. Extended abstract: Springer Lecture Notes in Computer Science, vol. 173. Full version: Technical Report UCAM-CL-TR-51, University of Cambridge, Computer Laboratory (1984)
Winskel, G., Zappa Nardelli, F.: new-HOPLA: a higher-order process language with name generation. In: Proc. of 3rd IFIP TCS, pp. 521–534 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Turner, D., Winskel, G. (2009). Nominal Domain Theory for Concurrency. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_39
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)