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
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.