@inproceedings{c61d84b19efb4d1499c34ed33a87742f,
title = "ProofViz: An Interactive Visual Proof Explorer",
abstract = "We introduce ProofViz, an extension to the Cur proof assistant that enables interactive visualization and exploration of in-progress proofs. The tool displays a representation of the underlying proof tree, information about each node in the tree, and the partially-completed proof term at each node. Users can interact with the proof by executing tactics, changing the focus, or undoing previous actions. We anticipate that ProofViz will be useful both to students new to tactic-based theorem provers, and to advanced users developing new tactics.",
keywords = "GUI tools, IDEs, Proof assistants",
author = "Daniel Melcer and Stephen Chang",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 22nd International Symposium on Trends in Functional Programming, TFP 2021 ; Conference date: 17-02-2021 Through 19-02-2021",
year = "2021",
doi = "10.1007/978-3-030-83978-9\_6",
language = "English",
isbn = "9783030839772",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "116--135",
editor = "Viktoria Zsok and John Hughes",
booktitle = "Trends in Functional Programming - 22nd International Symposium, TFP 2021, Revised Selected Papers",
}