Daniel Melcer

Student at Northeastern University

Daniel Melcer is a computer science undergraduate at Northeastern University in Boston, MA, USA. As a prospective PhD student, he would like to do research that uses programming languages to push boundaries in machine learning. In his free time, he enjoys biking, reading science fiction, and listening to weird music.

ProofViz: An Interactive Visual Proof Explorer

AUTHORS: Daniel Melcer and Stephen Chang:

ProofViz: An Interactive Visual Proof Explorer  We introduce ProofViz, an extension to the Cur proof assistant ecosystem 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 values of partially-completed proof terms. Users can interact with the proof by executing tactics, changing the focus to any hole, and undoing or redoing their previous interactions.

We anticipate that ProofViz will be useful both as a tool to introduce tactic proofs to learners of dependent type systems,  and as a mechanism for advanced users looking for insight into the effects of their custom tactics.  

OBJECTIVE: Demonstrate the need for a tool that exposes how tactics interact with the internal tree structure of a proof, and introduce a tool that does so.  

AUDIENCE: People interested in tactic-based proof systems and dependent types.

Slides
←Back