MikiBeta: A General GUI Library for Visualizing Proof Trees

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 a rule to apply, without worrying about rewriting various parts of a proof tree through unification, copying similar expressions for each judgement, or how much space is necessary to complete proof trees. To cope with many different kinds of proof trees, MikiBeta is designed to work with user-defined judgements and inference rules. Although MikiBeta is still in its infancy, we have used it to visualize typing derivations for the simply-typed lambda calculus extended with delimited continuation constructs, system F, as well as logical proof trees for sequent calculus.