Document Open Access Logo

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Authors Murdoch J. Gabbay, Dan R. Ghica, Daniela Petrisan

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.374.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Murdoch J. Gabbay
Dan R. Ghica
Daniela Petrisan

Cite As Get BibTex

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.374

Abstract

We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.

Subject Classification

Keywords
  • nominal sets
  • scope
  • alpha equivalence
  • dynamic sequences

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electr. Notes Theor. Comput. Sci., 3:2-14, 1996. Google Scholar
  2. Henk P. Barendregt. The Lambda Calculus: its Syntax and Semantics (revised ed.). North-Holland, 1984. Google Scholar
  3. Nick Benton and Benjamin Leperchey. Relational reasoning in a nominal semantics for storage. In Typed Lambda Calculi and Applications, pages 86-101. Springer, 2005. Google Scholar
  4. Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Logical Methods in Comp. Sci., 10(3), 2014. Google Scholar
  5. Mikołaj Bojańczyk. Nominal monoids. Theory of Computing Systems, 53(2):194-222, 2013. Google Scholar
  6. Ranald Clouston. Nominal lawvere theories: A category theoretic account of equational theories with names. J. Comput. Syst. Sci., 80(6):1067-1086, 2014. Google Scholar
  7. Ranald A. Clouston and Andrew M. Pitts. Nominal equational logic. Electr. Notes Theor. Comput. Sci., 172:223-257, 2007. Google Scholar
  8. Maribel Fernández and Murdoch J. Gabbay. Nominal rewriting (journal version). Information and Computation, 205(6):917-965, June 2007. Google Scholar
  9. Murdoch Gabbay and Dan R. Ghica. Game semantics in the nominal model. Electr. Notes Theor. Comput. Sci., 286:173-189, 2012. Google Scholar
  10. Murdoch J. Gabbay. A general mathematics of names. Information and Computation, 205(7):982-1011, July 2007. Google Scholar
  11. Murdoch J. Gabbay. Nominal algebra and the HSP theorem. Journal of Logic and Computation, 19(2):341-367, April 2009. Google Scholar
  12. Murdoch J. Gabbay. Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic, 17(2):161-229, 2011. Google Scholar
  13. Murdoch J. Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In FOSSACS, volume 6604 of Lec. Notes in Comp. Sci., pages 365-380. Springer, 2011. Google Scholar
  14. Murdoch J. Gabbay and Aad Mathijssen. Nominal universal algebra: equational logic with names and binding. Journal of Logic and Computation, 19(6):1455-1508, December 2009. Google Scholar
  15. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13(3-5):341-363, July 2001. Google Scholar
  16. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic, 151(2-3):89-114, 2008. Google Scholar
  17. Dimitri Hendriks and Vincent van Oostrom. adbmal. In CADE, volume 2741 of Lec. Notes in Comp. Sci., pages 136-150. Springer, 2003. Google Scholar
  18. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. Inf. Comput., 163(2):285-408, 2000. Google Scholar
  19. Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene coalgebra. In M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann, editors, Proc. 42nd Int. Colloq. Automata, Languages, and Programming, Part II (ICALP 2015), volume 9135 of Lecture Notes in Computer Science, pages 290-302, Kyoto, Japan, July 6-10 2015. EATCS, Springer. Google Scholar
  20. Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. Technical report, Computing and Information Science, Cornell University, November 2014. Google Scholar
  21. Alexander Kurz and Daniela Petrisan. On universal algebra over nominal sets. Math. Struc. in Comp. Sci., 20(2):285-318, 2010. Google Scholar
  22. Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Logical Methods in Computer Science, 9(4), 2013. Google Scholar
  23. Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. On nominal regular languages with binders. In FOSSACS, volume 7213 of Lec. Notes in Comp. Sci., pages 255-269. Springer, 2012. Google Scholar
  24. Andrew M Pitts. Nominal Sets: Names and Symmetry in Comp. Sci., volume 57. Cambridge University Press, 2013. Google Scholar
  25. Mark R Shinwell and Andrew M Pitts. On a monadic semantics for freshness. Theor. Comp. Sci., 342(1):28-55, 2005. Google Scholar
  26. Nikos Tzevelekos. Fresh-register automata. In POPL, pages 295-306. ACM, 2011. Google Scholar
  27. Christian Urban. Nominal reasoning techniques in Isabelle/HOL. J. of Automatic Reasoning, 40(4):327-356, 2008. Google Scholar
  28. Albert Visser, Kees Vermeulen, et al. Dynamic bracketing and discourse representation. Notre Dame Journal of Formal Logic, 37(2):321-365, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact