License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.4
URN: urn:nbn:de:0030-drops-138996
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13899/
Go to the corresponding LIPIcs Volume Portal


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

A Graphical User Interface Framework for Formal Verification

pdf-format:
LIPIcs-ITP-2021-4.pdf (1 MB)


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.

BibTeX - Entry

@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4,
  author =	{Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.},
  title =	{{A Graphical User Interface Framework for Formal Verification}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13899},
  URN =		{urn:nbn:de:0030-drops-138996},
  doi =		{10.4230/LIPIcs.ITP.2021.4},
  annote =	{Keywords: User Interfaces, ITP}
}

Keywords: User Interfaces, ITP
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: The supplementary material presented with this paper is incorporated into the leanprover-community GitHub repositories.
Software (Server): https://github.com/leanprover-community/lean/tree/master/library/init/meta/widget archived at: https://archive.softwareheritage.org/swh:1:dir:65d6fe171a7697793be204922aba83f2a94f5d20
Software (Client): https://github.com/leanprover/vscode-lean/blob/master/infoview/widget.tsx archived at: https://archive.softwareheritage.org/swh:1:cnt:e713dbc30927867464effc1e51fd1230cd961cbd


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI