Document Open Access Logo

Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure

Authors Lawrence Dunn , Val Tannen , Steve Zdancewic

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.14.pdf
  • Filesize: 1.07 MB
  • 20 pages

Document Identifiers

Author Details

Lawrence Dunn
  • University of Pennsylvania, Philadelphia, PA, USA
Val Tannen
  • University of Pennsylvania, Philadelphia, PA, USA
Steve Zdancewic
  • University of Pennsylvania, Philadelphia, PA, USA

Acknowledgements

We wish to thank the anonymous reviewers for their helpful comments and suggestions, and the authors of LNgen for describing their work and experience using LNgen.

Cite AsGet BibTex

Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.14

Abstract

Verifying the metatheory of a formal system in Coq involves a lot of tedious "infrastructural" reasoning about variable binders. We present Tealeaves, a generic framework for first-order representations of variable binding that can be used to develop this sort of infrastructure once and for all. Given a particular strategy for representing binders concretely, such as locally nameless or de Bruijn indices, Tealeaves allows developers to implement modules of generic infrastructure called backends that end users can simply instantiate to their own syntax. Our framework rests on a novel abstraction of first-order abstract syntax called a decorated traversable monad (DTM) whose equational theory provides reasoning principles that replace tedious induction on terms. To evaluate Tealeaves, we have implemented a multisorted locally nameless backend providing generic versions of the lemmas generated by LNgen. We discuss case studies where we instantiate this generic infrastructure to simply-typed and polymorphic lambda calculi, comparing our approach to other utilities.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • Coq
  • category theory
  • formal metatheory
  • raw syntax
  • locally nameless

Metrics

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

Supplementary Materials

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, 1991. URL: https://doi.org/10.1017/S0956796800000186.
  2. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases: The Logical Level. Addison-Wesley Longman Publishing Co., Inc., USA, 1st edition, 1995. Google Scholar
  3. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Journal of Functional Programming, 31:e22, 2021. URL: https://doi.org/10.1017/S0956796820000076.
  4. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453-468. Springer, 1999. URL: https://doi.org/10.1007/3-540-48168-0_32.
  5. Brian Aydemir and Stephanie Weirich. LNgen: Tool Support for Locally Nameless Representations. Technical report, University of Pennsylvania, Department of Computer and Information Science, June 2010. URL: https://repository.upenn.edu/cis_reports/933/.
  6. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The poplmark challenge. In Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'05, pages 50-65, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/11541868_4.
  7. Françoise Bellegarde and James Hook. Substitution: A formal methods case study using monads and transformations. Sci. Comput. Program., 23(2–3):287-311, December 1994. URL: https://doi.org/10.1016/0167-6423(94)00022-0.
  8. Richard Bird, Jeremy Gibbons, Stefan Mehner, Janis Voigtländer, and Tom Schrijvers. Understanding idiomatic traversals backwards and forwards. SIGPLAN Not., 48(12):25-36, September 2013. URL: https://doi.org/10.1145/2578854.2503781.
  9. Richard S. Bird and Ross Paterson. De bruijn notation as a nested datatype. J. Funct. Program., 9(1):77-91, 1999. URL: https://doi.org/10.1017/s0956796899003366.
  10. Rod M. Burstall. Proving properties of programs by structural induction. Comput. J., 12(1):41-48, 1969. URL: https://doi.org/10.1093/comjnl/12.1.41.
  11. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/s10817-011-9225-2.
  12. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, pages 143-156, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1411204.1411226.
  13. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  14. David Delahaye. A tactic language for the system coq. In Michel Parigot and Andrei Voronkov, editors, Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings, volume 1955 of Lecture Notes in Computer Science, pages 85-95. Springer, 2000. URL: https://doi.org/10.1007/3-540-44404-1_7.
  15. Marcelo Fiore. Second-order and dependently-sorted abstract syntax. In Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, LICS '08, pages 57-68, USA, 2008. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2008.38.
  16. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 193-202. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
  17. Marcelo Fiore and Dmitrij Szamozvancev. Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498715.
  18. Jeremy Gibbons and Bruno Oliveira. The essence of the iterator pattern. J. Funct. Program., 19:377-402, July 2009. URL: https://doi.org/10.1017/S0956796809007291.
  19. Yuri Gurevich and Saharon Shelah. Fixed-point extensions of first-order logic. Annals of Pure and Applied Logic, 32(nil):265-280, 1986. URL: https://doi.org/10.1016/0168-0072(86)90055-2.
  20. Mauro Jaskelioff and Russell O'Connor. A representation theorem for second-order functionals. Journal of Functional Programming, 25, February 2014. URL: https://doi.org/10.1017/S0956796815000088.
  21. Mauro Jaskelioff and Ondrej Rypacek. An investigation of the laws of traversals. Electronic Proceedings in Theoretical Computer Science, 76, February 2012. URL: https://doi.org/10.4204/EPTCS.76.5.
  22. C. Barry Jay and J. Robin B. Cockett. Shapely types and shape polymorphism. In Donald Sannella, editor, Programming Languages and Systems - ESOP'94, 5th European Symposium on Programming, Edinburgh, UK, April 11-13, 1994, Proceedings, volume 788 of Lecture Notes in Computer Science, pages 302-316. Springer, 1994. URL: https://doi.org/10.1007/3-540-57880-3_20.
  23. Gyesik Lee, Bruno C. D. S. Oliveira, Sungkeun Cho, and Kwangkeun Yi. GMeta: A generic formal metatheory framework for first-order representations. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of Lecture Notes in Computer Science, pages 436-455. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_22.
  24. Conor McBride. Type-preserving renaming and substitution. Unpublished note, 2005. URL: http://strictlypositive.org/ren-sub.pdf.
  25. Conor McBride and Ross Paterson. Applicative programming with effects. J. Funct. Program., 18(1):1-13, January 2008. URL: https://doi.org/10.1017/S0956796807006326.
  26. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Richard L. Wexelblat, editor, Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, pages 199-208. ACM, 1988. URL: https://doi.org/10.1145/53990.54010.
  27. Clément Pit-Claudel. Untangling mechanized proofs. In Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, pages 155-174, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3426425.3426940.
  28. Andrew M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186(2):165-193, 2003. Theoretical Aspects of Computer Software (TACS 2001). URL: https://doi.org/10.1016/S0890-5401(03)00138-X.
  29. Randy Pollack. Closure under alpha-conversion. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 313-332, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg. Google Scholar
  30. Randy Pollack. Reasoning about languages with binding: Can we do it yet?, February 2006. URL: https://web.archive.org/web/20101122040606/http://homepages.inf.ed.ac.uk/rpollack/export/bindingChallenge_slides.pdf.
  31. François Pottier and Coq maintainers. DBlib. https://github.com/coq-community/dblib, 2019.
  32. Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de bruijn terms and parallel substitutions. In Xingyuan Zhang and Christian Urban, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, LNAI. Springer-Verlag, August 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_24.
  33. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective tool support for the working semanticist. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP '07, pages 1-12, New York, NY, USA, 2007. Association for Computing Machinery. URL: https://doi.org/10.1145/1291151.1291155.
  34. Matthieu Sozeau and Nicolas Oury. First-class type classes. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs '08, pages 278-293, Berlin, Heidelberg, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  35. Bas Spitters and Eelis Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21, February 2011. URL: https://doi.org/10.1017/S0960129511000119.
  36. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: Reasoning with multi-sorted de bruijn terms and vector substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 166-180, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294101.
  37. Christian Urban and Christine Tasson. Nominal techniques in isabelle/hol. In Robert Nieuwenhuis, editor, Automated Deduction - CADE-20, pages 38-53, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11532231_4.
  38. Philip Wadler. The essence of functional programming. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '92, pages 1-14, New York, NY, USA, 1992. Association for Computing Machinery. URL: https://doi.org/10.1145/143165.143169.
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