Document Open Access Logo

Nominal Techniques for Software Specification and Verification (Invited Talk)

Author Maribel Fernández

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.1.pdf
  • Filesize: 464 kB
  • 4 pages

Document Identifiers

Author Details

Maribel Fernández
  • Department of Informatics, King’s College London, UK

Funding

This work is partially funded by the Royal Society (International Exchanges, grant number IES$$1R2$$1212106).

Acknowledgements

The work described in this abstract is the result of collaborations with several researchers, cited below. Special thanks to my PhD students and co-authors.

Cite AsGet BibTex

Maribel Fernández. Nominal Techniques for Software Specification and Verification (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.1

Abstract

In this talk we discuss the nominal approach to the specification of languages with binders and some applications to programming languages and verification.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Lambda calculus
  • Theory of computation → Equational logic and rewriting
Keywords
  • Binding operator
  • Nominal Logic
  • Nominal Rewriting
  • Unification
  • Equational Theories
  • Type Systems

Metrics

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

References

  1. Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho, and Ana Oliveira. A formalisation of nominal α-equivalence with A, C, and AC symbols. Theor. Comput. Sci., 781:3-23, 2019. URL: https://doi.org/10.1016/j.tcs.2019.02.020.
  2. Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes-Sobrinho. Formalising nominal C-unification generalised with protected variables. Math. Struct. Comput. Sci., 31(3):286-311, 2021. URL: https://doi.org/10.1017/S0960129521000050.
  3. Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, page 11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  4. Maurício Ayala-Rincón, Maribel Fernández, Ana Cristina Rocha-Oliveira, and Daniel Lima Ventura. Nominal essential intersection types. Theoretical Computer Science, 737:62-80, 2018. URL: https://doi.org/10.1016/j.tcs.2018.05.008.
  5. Jesper Bengtson and Joachim Parrow. Formalising the pi-calculus using nominal logic. LMCS, 5(2), 2009. URL: http://arxiv.org/abs/0809.3960.
  6. Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 289-299. IEEE Computer Society, 1990. Google Scholar
  7. Christophe Calvès and Maribel Fernández. A polynomial nominal unification algorithm. Theor. Comp. Sci., 403:285-306, August 2008. Google Scholar
  8. Christophe Calvès and Maribel Fernández. Matching and alpha-equivalence check for nominal terms. Journal of Comp. Syst. Sci., 76(5):283-301, 2010. Google Scholar
  9. Christophe Calvès and Maribel Fernández. The first-order nominal link. In Logic-Based Program Synthesis and Transformation - 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers, volume 6564 of LNCS, pages 234-248. Springer, 2011. Google Scholar
  10. James Cheney. A dependent nominal type theory. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  11. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott, editors. All About Maude - A High-Performance Logical Framework, volume 4350 of LNCS. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  12. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, and Carolyn L. Talcott. Programming and symbolic computation in Maude. J. Log. Algebr. Meth. Program., 110, 2020. Google Scholar
  13. François Fages. Associative-Commutative Unification. In Robert E. Shostak, editor, 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, volume 170 of LNCS, pages 194-208. Springer, 1984. Google Scholar
  14. François Fages. Associative-Commutative Unification. J. of Sym. Computation, 3(3):257-275, 1987. Google Scholar
  15. Elliot Fairweather and Maribel Fernández. Typed nominal rewriting. ACM Transactions on Computational Logic, 19(1):6:1-6:46, 2018. URL: https://doi.org/10.1145/3161558.
  16. Elliot Fairweather, Maribel Fernández, Nora Szasz, and Alvaro Tasistro. Dependent types for nominal terms with atom substitutions. In Typed Lambda Calculus and Applications (Proceedings of TLCA), pages 180-195, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.180.
  17. Maribel Fernández and Murdoch J. Gabbay. Nominal rewriting. Inf. Comput., 205(6):917-965, 2007. Google Scholar
  18. Maribel Fernández and Murdoch J. Gabbay. Closed nominal rewriting and efficiently computable nominal algebra equality. In LFMTP, 2010. Google Scholar
  19. Maribel Fernández, Murdoch J. Gabbay, and Ian Mackie. Nominal rewriting systems. In PPDP, pages 108-119. ACM Press, August 2004. Google Scholar
  20. Murdoch J. Gabbay. Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic, 2011. Google Scholar
  21. 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
  22. Jordi Levy and Mateu Villaret. An efficient nominal unification algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 209-226. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  23. Andrzej S. Murawski and Nikos Tzevelekos. Nominal game semantics. FTPL, 2:4:191-269, 2016. URL: https://doi.org/10.1561/2500000017.
  24. Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reasoning, 55(1):1-37, 2015. URL: https://doi.org/10.1007/s10817-015-9322-8.
  25. Andrew M. Pitts. Nominal logic: A first order theory of names and binding. In TACS, volume 2215 of LNCS, pages 219-242. Springer, 2001. Google Scholar
  26. Andrew M Pitts. Nominal sets: Names and symmetry in computer science. Cambridge UP, 2013. Google Scholar
  27. Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with bound names modulo renaming. In Proceedings of the 5th international conference on the mathematics of program construction (MPC 2000), volume 1837 of LNCS, pages 230-255. Springer, December 2000. URL: http://www.gabbay.org.uk/papers.html#metpbn.
  28. Andrew M. Pitts, Justus Matthiesen, and Jasper Derikx. A dependent type theory with abstractable names. Electr. Notes Theor. Comput. Sci., 312:19-50, 2015. URL: https://doi.org/10.1016/j.entcs.2015.04.003.
  29. Grigore Rosu and Traian-Florin Serbanuta. An overview of the K semantic framework. J. Log. Algebr. Program., 79(6):397-434, 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  30. Ulrich Schöpp and Ian Stark. A Dependent Type Theory with Names and Binding. In CSL, pages 235-249, 2004. Google Scholar
  31. Mark Stickel. A Unification Algorithm for Associative-Commutative Functions. J. of the ACM, 28(3):423-434, 1981. Google Scholar
  32. Mark E. Stickel. A Complete Unification Algorithm for Associative-Commutative Functions. In Advance Papers of the Fourth International Joint Conference on Artificial Intelligence, Tbilisi, Georgia, USSR, September 3-8, 1975, pages 71-76, 1975. Google Scholar
  33. Christian Urban. Nominal techniques in Isabelle/HOL. J. Autom. Reason., 40(4):327-356, May 2008. Google Scholar
  34. Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay. Nominal unification. In CSL, volume 2803 of LNCS, pages 513-527. Springer, December 2003. URL: http://www.gabbay.org.uk/papers.html#nomu, URL: https://doi.org/10.1016/j.tcs.2004.06.016.
  35. Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay. Nominal unification. Theor. Comp. Sci., 323(1-3):473-497, 2004. URL: https://doi.org/10.1016/j.tcs.2004.06.016.
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 Imprint Privacy Contact