Freshness and Name-Restriction in Sets of Traces with Names

  • Murdoch J. Gabbay
  • Vincenzo Ciancia
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6604)


We use nominal sets (sets with names and binding) to define a framework for trace semantics with dynamic allocation of resources.

Using novel constructions in nominal sets, including the technical devices of positive nominal sets and maximal planes, we define notions of capture-avoiding composition and name-restriction on sets of traces with names.

We conclude with an extended version of Kleene algebras which summarises in axiomatic form the relevant properties of the constructions.


  1. 1.
    Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.-H.L., Stark, I.D.B.: Nominal games and full abstraction for the nu-calculus. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 150–159. IEEE Computer Society Press, Los Alamitos (2004)CrossRefGoogle Scholar
  2. 2.
    Bonsangue, M., Kurz, A.: Pi-calculus in logical form. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp. 303–312. IEEE Computer Society Press, Los Alamitos (2007)CrossRefGoogle Scholar
  3. 3.
    Ciancia, V., Montanari, U.: Symmetries, local names and dynamic (de)-allocation of names, Information and Computation (2010) (in press)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Ciancia, V., Tuosto, E.: A novel class of automata for languages on infinite alphabets, Tech. Report CS-09-003, University of Leicester, UK (2009)Google Scholar
  5. 5.
    Fernández, M., Gabbay, Murdoch J.: Nominal rewriting with name generation: abstraction vs. locality. In: Proceedings of the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP 2005), pp. 47–58. ACM Press, New York (July 2005)Google Scholar
  6. 6.
    Fiore, M., Moggi, E., Sangiorgi, D.: A fully-abstract model for the π-calculus (extended abstract). In: Proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 43–54. IEEE Computer Society Press, Los Alamitos (1996)CrossRefGoogle Scholar
  7. 7.
    Fiore, M., Staton, S.: Comparing operational models of name-passing process calculi. Information and Computation 204(4), 524–560 (2006)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Fiore, M., Turi, D.: Semantics of name and value passing. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 93–104. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  9. 9.
    Francez, N., Hoare, C.A.R., Lehmann, D.J., de Roever, W.P.: Semantics of nondeterminism, concurrency, and communication. Journal of Computer and System Sciences 19(3), 290–308 (1979)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Gabbay, Murdoch J.: A Theory of Inductive Definitions with alpha-Equivalence, Ph.D. thesis, University of Cambridge, UK (March 2001)Google Scholar
  11. 11.
    Gabbay, Murdoch J.: A General Mathematics of Names. Information and Computation 205(7), 982–1011 (2007)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Gabbay, Murdoch J.: A study of substitution, using nominal techniques and Fraenkel-Mostowski sets. Theoretical Computer Science 410(12-13), 1159–1189 (2009)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Gabbay, Murdoch J.: Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic (2010) (in press)Google Scholar
  14. 14.
    Gabbay, Murdoch J., Mathijssen, A.: Nominal universal algebra: equational logic with names and binding. Journal of Logic and Computation 19(6), 1455–1508 (2009)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Gabbay, Murdoch J., Pitts, A.M.: A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13(3-5), 341–363 (2001)CrossRefGoogle Scholar
  16. 16.
    Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras (pre)sheaves and named sets. Higher-Order and Symbolic Computation 19(2-3), 283–304 (2006)CrossRefGoogle Scholar
  17. 17.
    Holzmann, G.J.: The spin model checker: Primer and reference manual. Addison-Wesley Professional, Reading (September 2003)Google Scholar
  18. 18.
    Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2), 329–363 (1994)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Kozen, D.: On induction vs. *-continuity. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 167–176. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  20. 20.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Principles and Practice of Declarative Programming, 5th International ACM SIGPLAN Symposium (PPDP 2003), pp. 184–194. ACM, New York (2003)Google Scholar
  22. 22.
    Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Montanari, U., Pistore, M.: π-Calculus, Structured Coalgebras and Minimal HD-Automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, p. 569. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Odersky, M.: A functional theory of local names. In: Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages (POPL 1994), pp. 48–59. ACM Press, New York (1994)Google Scholar
  25. 25.
    Pitts, A.M., Stark, I.D.B.: Observable properties of higher order functions that dynamically create local names, or: What’s new? In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 122–141. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  26. 26.
    Pitts, A.M.: Nominal system T. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 159–170. ACM Press, New York (January 2010)Google Scholar
  27. 27.
    Pitts, A.M., Gabbay, Murdoch J.: A Metalanguage for Programming with Bound Names Modulo Renaming. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 230–255. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  28. 28.
    Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. Theoretical Computer Science 342(1), 28–55 (2005)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Shinwell, M.R., Pitts, A.M., Gabbay, Murdoch J.: FreshML: Programming with Binders Made Simple. In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), vol. 38, pp. 263–274. ACM Press, New York (August 2003)Google Scholar
  30. 30.
    Tzevelekos, N.: Nominal game semantics. Ph.D. thesis, Oxford (2008)Google Scholar
  31. 31.
    Tzevelekos, N.: Fresh-register automata. In: Proceedings of the 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2011). ACM Press, New York (January 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Murdoch J. Gabbay
  • Vincenzo Ciancia

There are no affiliations available

Personalised recommendations