MikiBeta : A general GUI library for visualizing proof trees. System description and demonstration. This paper describes and demonstrates MikiBeta, a general graphical user interface (GUI) library we are developing for visualizing proof trees. Using MikiBeta, one can construct a proof tree step by step by selecting a judgement and clicking an inference rule to apply, without worrying about instanciating metavariables with their contents, copying similar expressions for each judgement, or how much space is necessary to visualize the complete proof tree. To cope with different kinds of proof trees, MikiBeta is parameterized with user-defined judgements and inference rules. Because MikiBeta allows arbitrary side-effect-free user code in inference rules, one can construct GUIs with complex operations such as environment lookup and substitution. We have successfully visualized typing derivations for $lambda $ calculi with let polymorphism and with shift and reset, System F, as well as a simple deduction system for Combinatory Logic.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element