Show simple item record

dc.contributor.authorAyers, EW
dc.contributor.authorJamnik, M
dc.contributor.authorGowers, WT
dc.date.accessioned2022-01-22T00:30:53Z
dc.date.available2022-01-22T00:30:53Z
dc.date.issued2021-06-01
dc.identifier.isbn9783959771887
dc.identifier.issn1868-8969
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/332871
dc.description.abstractWe 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.
dc.publisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
dc.relation.ispartofseriesLIPIcs
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleA graphical user interface framework for formal verification
dc.typeConference Object
dc.publisher.departmentDepartment of Computer Science And Technology
dc.date.updated2022-01-19T16:43:22Z
prism.endingPage4:1
prism.publicationDate2021
prism.publicationNameLeibniz International Proceedings in Informatics, LIPIcs
prism.startingPage4:1
prism.volume193
dc.identifier.doi10.17863/CAM.80301
dcterms.dateAccepted2021-04-14
rioxxterms.versionofrecord10.4230/LIPIcs.ITP.2021.4
rioxxterms.versionVoR
dc.contributor.orcidJamnik, Mateja [0000-0003-2772-2532]
dc.contributor.orcidGowers, William [0000-0002-5168-0785]
pubs.conference-nameITP
cam.orpheus.success2022-03-01: VoR added to Apollo record
cam.depositDate2022-01-19
pubs.licence-identifierapollo-deposit-licence-2-1
pubs.licence-display-nameApollo Repository Deposit Licence Agreement


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International