A graphical user interface framework for formal verification
View / Open Files
Authors
Ayers, EW
Jamnik, M
Gowers, WT
Publication Date
2021-06-01Journal Title
Leibniz International Proceedings in Informatics, LIPIcs
Conference Name
ITP
Series
LIPIcs
ISSN
1868-8969
ISBN
9783959771887
Publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Volume
193
Pages
4:1-4:1
Type
Conference Object
This Version
VoR
Metadata
Show full item recordCitation
Ayers, E., Jamnik, M., & Gowers, W. (2021). A graphical user interface framework for formal verification. Leibniz International Proceedings in Informatics, LIPIcs, 193 4:1-4:1. 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 leanprover-community fork of Lean 3. The framework is already in use by hundreds of contributors to the Lean mathematical library.
Identifiers
External DOI: https://doi.org/10.4230/LIPIcs.ITP.2021.4
This record's URL: https://www.repository.cam.ac.uk/handle/1810/332871
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.