Document Open Access Logo

A Graphical User Interface Framework for Formal Verification

Authors Edward W. Ayers , Mateja Jamnik , W. T. Gowers

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.4.pdf
  • Filesize: 1.44 MB
  • 16 pages

Document Identifiers

Author Details

Edward W. Ayers
  • DPMMS, University of Cambridge, UK
Mateja Jamnik
  • Department of Computer Science and Technology, University of Cambridge, UK
W. T. Gowers
  • DPMMS, University of Cambridge, UK

Funding

  • Ayers, Edward W.: EPSRC 1804138.

Acknowledgements

Enormous thanks to Gabriel Ebner and Brian Gen-ge Chen for reviewing the PRs and polishing the implementation. Also thanks for using the framework to create their own widgets, contributing and suggesting improvements: Daniel Fabian; Robert Y. Lewis; Markus Himmel; Minchao Wu; Kendall Frey; Patrick Massot.

Cite AsGet BibTex

Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.4

Abstract

We present the "ProofWidgets" framework for implementing general user interfaces (UIs) within an interactive theorem prover. The framework uses web technology and functional reactive programming, as well as metaprogramming features of advanced interactive theorem proving (ITP) systems to allow users to create arbitrary interactive UIs for representing the goal state. Users of the framework can create GUIs declaratively within the ITP’s metaprogramming language, without having to develop in multiple languages and without coordinated changes across multiple projects, which improves development time for new designs of UI. The ProofWidgets framework also allows UIs to make use of the full context of the theorem prover and the specialised libraries that ITPs offer, such as methods for dealing with expressions and tactics. The framework includes an extensible structured pretty-printing engine that enables advanced interaction with expressions such as interactive term rewriting. We exemplify the framework with an implementation for the https://leanprover-community.github.io. The framework is already in use by hundreds of contributors to the Lean mathematical library.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software usability
Keywords
  • User Interfaces
  • ITP

Metrics

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

Supplementary Materials

References

  1. Engineer Bainomugisha, Andoni Lombide Carreton, Tom Van Cutsem, Stijn Mostinckx, and Wolfgang De Meuter. A survey on reactive programming. ACM Comput. Surv., 45(4):52:1-52:34, 2013. URL: https://doi.org/10.1145/2501654.2501666.
  2. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci., 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:8)2018.
  3. Jon Barwise and John Etchemendy. Hyperproof: Logical reasoning with diagrams. In Working Notes of the AAAI Spring Symposium on Reasoning with Diagrammatic Representations, 1992. URL: https://www.aaai.org/Papers/Symposia/Spring/1992/SS-92-02/SS92-02-016.pdf.
  4. Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. J. Symb. Comput., 25(2):161-194, 1998. URL: https://doi.org/10.1006/jsco.1997.0171.
  5. Joachim Breitner. Visual theorem proving with the incredible proof machine. In Jasmin Christian Blanchette and Stephan Merz, editors, Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, volume 9807 of Lecture Notes in Computer Science, pages 123-139. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-43144-4_8.
  6. Evan Czaplicki and Stephen Chong. Asynchronous functional reactive programming for guis. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 411-422. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462161.
  7. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes Mathematicae (Proceedings), volume 75, pages 381-392. North-Holland, 1972. URL: http://alexandria.tue.nl/repository/freearticles/597619.pdf.
  8. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP):34:1-34:29, 2017. URL: https://doi.org/10.1145/3110278.
  9. Conal Elliott and Paul Hudak. Functional reactive animation. In Simon L. Peyton Jones, Mads Tofte, and A. Michael Berman, editors, Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), Amsterdam, The Netherlands, June 9-11, 1997, pages 263-273. ACM, 1997. URL: https://doi.org/10.1145/258948.258973.
  10. Emilio Jesús Gallego Arias. Serapi: Machine-friendly, data-centric serialization for coq. Technical report, MINES ParisTech, 2016. URL: https://core.ac.uk/download/pdf/51221893.pdf.
  11. Emilio Jesús Gallego Arias, Benoît Pin, and Pierre Jouvelot. jscoq: Towards hybrid theorem proving interfaces. In Serge Autexier and Pedro Quaresma, editors, Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, volume 239 of Electronic Proceedings in Theoretical Computer Science, pages 15-27. Open Publishing Association, 2017. URL: https://doi.org/10.4204/EPTCS.239.2.
  12. Mike Gordon. From LCF to HOL: a short history. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 169-186. The MIT Press, 2000. Google Scholar
  13. Robert Y. Lewis. An extensible ad hoc interface between lean and mathematica. In Catherine Dubois and Bruno Woltzenlogel Paleo, editors, Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017, volume 262 of EPTCS, pages 23-37, 2017. URL: https://doi.org/10.4204/EPTCS.262.4.
  14. Helen Lowe and David Duncan. Xbarnacle: Making theorem provers more accessible. In William McCune, editor, Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, volume 1249 of Lecture Notes in Computer Science, pages 404-407. Springer, 1997. URL: https://doi.org/10.1007/3-540-63104-6_39.
  15. Christoph Lüth and Martin Ring. A web interface for isabelle: The next generation. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings, volume 7961 of Lecture Notes in Computer Science, pages 326-329. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39320-4_22.
  16. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  17. John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Commun. ACM, 3(4):184-195, 1960. URL: https://doi.org/10.1145/367177.367199.
  18. Clément Pit-Claudel. Untangling mechanized proofs. In Ralf Lämmel, Laurence Tratt, and Juan de Lara, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, November 16-17, 2020, pages 155-174. ACM, 2020. URL: https://doi.org/10.1145/3426425.3426940.
  19. Jörg H. Siekmann, Stephan M. Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, and Volker Sorge. LOUI: Lovely omega user interface. Formal Aspects Comput., 11(3):326-342, 1999. URL: https://doi.org/10.1007/s001650050053.
  20. Sebastian Ullrich and Leonardo de Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 167-182. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_10.
  21. Makarius Wenzel. Isabelle/jedit - A prover IDE within the PIDE framework. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of Lecture Notes in Computer Science, pages 468-471. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31374-5_38.
  22. Makarius Wenzel. Isabelle/pide after 10 years of development. In UITP workshop: User Interfaces for Theorem Provers., 2018. URL: https://sketis.net/wp-content/uploads/2018/08/isabellepide-uitp2018.pdf.
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