Mikiβ : A General GUI Libraryfor Visualizing Proof Trees– System Description and Demonstration –Kanako Sakurai and Kenichi Asai
Ochanomizu University, Japan{sakurai.kanako,asai}@is.ocha.ac.jp

Abstract. This paper describes and demonstrates Mikiβ, a general graphical user interface (GUI) library we are developing for visualizing proof
trees. Using Mikiβ, 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 uniﬁcation, copying similar expressions for each judgement, or how much space is necessary tocomplete proof trees. To cope with many diﬀerent kinds of proof trees,
Mikiβ is designed to work with user-deﬁned judgements and inference
rules. Although Mikiβ is still in its infancy, we have used it to visualize
typing derivations for the simply-typed lambda calculus extended withdelimited continuation constructs, system F, as well as logical proof trees
for sequent calculus.
Key words: graphical user interface (GUI), proof tree, type system,
lambda calculus, system F, sequent calculus, OCaml, LablTk

1

Introduction

A proof tree is used in various places. We write a proof tree to infer a type ofan expression and to prove a logical formula, for example. It is also useful for
educational purposes to understand the behavior of type systems and deduction
systems. However, writing a proof tree by hand is not so straightforward. It is
often diﬃcult to predict how big the proof tree will become. We also need tocopy similar expressions many times. Even worse, we have to rewrite almost
whole the tree when a metavariable is instantiated to something else because of
uniﬁcation.
These problems could be avoided if we construct a graphical user interface(GUI) for writing proof trees. However, writing one GUI is not enough. We
design new type systems for diﬀerent purposes, and we want to visualize proof
trees for these new systems, too. But those who design type systems want toconcentrate on type systems and do not usually want to bother themselves about
making GUI.
As an attempt to resolve this situation, we are developing a general GUI
system, Mikiβ, for visualizing proof trees. To use Mikiβ, one is required to supply

deﬁnition for judgements and inference rules in a speciﬁc way. Then, Mikiβ uses
the deﬁnition to construct a GUI system for it. Mikiβ is still an on-going workand requires users to write quite a lot of things. However they are mostly about
the inference system itself and not about GUI. Thus, we expect that Mikiβ users
can concentrate on the inference system itself to obtain GUI for it.
After showing the overview of Mikiβ in Section 2, we show how to construct a
GUI for the simply-typed lambda calculus as an example (Section 3). In Section
4, we show other systems we have implemented. We mention related work in
Section 5 and the paper concludes in Section 6.

2

Overview of Mikiβ

The ultimate goal of the Mikiβ project is to build a system in which a GUI is
constructed from the deﬁnition of judgements and inference rules. Toward thisgoal, the current Mikiβ aims at separating GUI parts from the deﬁnition ofinference rules as much as possible, so that users need not care about GUI verymuch to construct a GUI system.
Mikiβ is being developed with LablTk in OCaml. It oﬀers a data structure fora tree and related functions as well as a GUI library to initialize a window and toregister buttons. Since Mikiβ oﬀers only GUI-related functions, it does not oﬀerfunctions regarding inference rules. Thus, users of Mikiβ need to understand theinference rules deeply and deﬁne them properly.
To build a GUI system using Mikiβ, one has to provide a syntax of judgements (together with a lexer and parer) and four functions for:– extracting a GUI object identiﬁer,– generating a new metavariable,– uniﬁcation, and– drawing expressions
for each user-deﬁned data type.

3

Using Mikiβ

In this section, we use the simply-typed lambda calculus to show how to construct a GUI with Mikiβ. The syntax and typing rules are shown in Fig. 1.
The deﬁnition is standard except for the inclusion of (TWEAK). Usually, we avoid(TWEAK) by regarding a context Γ as a set of bindings. However, the precise
speciﬁcation would then require a deﬁnition of sets. Here, we represent Γ as anordered list of bindings and use (TWEAK) instead.
Note that variables appearing in typing rules (x, T, Γ, etc.) are metavariables. They are replaced with concrete values, when typing rules are applied toconstruct a proof tree.

Syntax
t ::=

T ::=

Γ ::=

j ::=

Typingterms:
xvariables
λx:T.tabstraction
t tapplication
types:
B
base type
T → T
type of functions
contexts:∅
empty context
x:T, Γ
variable bindingΓ ` t : T
judgements:

x : T, Γ ` x : T(TVAR)

x : T1 , Γ ` t : T2
Γ ` λx : T1 .t : T1 → T2

(TABS)

Γ ` t1 : T11 → T12 Γ ` t2 : T11
Γ ` t1 t2 : T12(TAPP)
Γ `t:Tx : T1 , Γ ` t : T(TWEAK)

Fig. 1. The simply-typed lambda calculus

3.1

Deﬁnition of Syntax

Mikiβ oﬀers a data type tree t of proof trees to be visualized in GUI.
type tree_t =Axiom of judge_t| Infer of judge_t * tree_t list (* assumptions *)The type judge t is a type for judgements to be deﬁned by Mikiβ users.
For the simply-typed lambda calculus, deﬁnition of judge t becomes as shownin Fig. 2 in the typewriter font. It is a straightforward transcription of Fig. 1
into OCaml, except that variables are assigned an independent type rather thanusing a raw string. This is because we want to assign single GUI object to thesemantically same variables.

type ’a meta t =string ref * ’a option ref * id t
type var t =V of string * id t
| MetaVar of var t meta t

type type t =TVar of string * id t
| Fun of type t * type t * id t
| MetaType of type t meta t
type env t =Empty of id t
| Cons ofvar t * type t * env t * id t
| MetaEnv of env t meta t

type term t =Var of var t * id t
| Abs of var t * term t * id t
| App of term t * term t * id t
type judge t =| MetaTerm of term t meta t
Judge of env t * term t * type t * id t
Fig. 2. The syntax deﬁnition of simply-typed lambda calculus in Mikiβ

For this type deﬁnition, we need to add two things to use it in Mikiβ. They
are shown in italic in Fig. 2.

GUI object identiﬁers Each constructor needs a GUI object identiﬁer id t.
It enables Mikiβ to relate OCaml data with GUI objects on a display. Users
do not need to know how the identiﬁer is deﬁned internally.
Metavariables In the typing rules of Fig. 1, each variable is regarded as ametavariable. To represent a metavariable, we add it to the type deﬁnitionin Fig. 2. For example, a metavariable for types is deﬁned as follows:
MetaType of type_t meta_t
where ’a meta t is deﬁned as follows:
type ’a meta_t = string ref * ’a option ref * id_t
A metavariable has a name and a pointer to another data of the same type.
When a metavariable is instantiated to a concrete value, the pointer tothe value is set in the metavariable. Mikiβ will oﬀer functions operating’a meta t.
Besides the above two additions, users are currently requested to write twomore functions as well as a lexer and a parser to convert concrete syntax into
the above data type. One is a function to extract an identiﬁer from data, andthe other is a function to generate a new metavariable. For example, we deﬁne
the two functions for type t data type as follows. Here, new meta is a function
to generate a new value of type ’a meta t using a given string.
(* Extracting id_t *)let get_type_id tp = match tp with
TVar(_, id) | Fun(_, _, id) | MetaType(_, _, id) -> id(* Generating a new metavariable *)let new_type () = MetaType(new_meta "T")3.2

Deﬁnition of Inference Rules

Thanks to the introduction of metavariables, users can directly deﬁne inference
rules as a tree structure. For example, (TABS) is deﬁned as follows. Here, NEW is
a predeﬁned dummy identiﬁer in Mikiβ.
let t_abs() =(* generating new metavaiables *)let e = new_env() in(* context *)let tm = new_term() in (* term *)let x = new_var() in(* variable *)let tp1 = new_type() in (* type *)let tp2 = new_type() in(* define the inference rule using metavariables *)Infer(Judge(e, Abs(x, tp1, tm, NEW), Fun(tp1, tp2, NEW), NEW),[Infer(Judge(Cons(x, tp1, e, NEW), tm, tp2, NEW), [])])

Whenever we need to supply a value of type id t, we use NEW. Assumptions of
the inference rules are encoded as a list of Infer nodes with an empty assumption
list. It indicates that we need to ﬁnd their proofs before completing a proof tree.
The other inference rules are written similarly. Inference rules deﬁned in thisway are registered to infer button list, which is used to create a button foreach inference rule on a display.
let infer_button_list = [("TVAR", t_var); ("TABS", t_abs);("TAPP", t_app); ("TWEAK", t_weak)]
3.3

Deﬁnition of Uniﬁcation and Application of Inference Rules

A proof tree is constructed in three steps:
1. selection of a judgement and an inference rule,
2. uniﬁcation of the judgement and the conclusion of the inference rule, and3. substitution of the judgement with the instantiated inference rule.
For example, application of (TABS) to a : int ` (λx : T1 .x) a : T2 (written inbold font) is depicted in Fig. 3.
a : int ` (λx : T1 .x) a : T2
(original proof tree)` λa : int.((λx : T1 .x) a) : int → T2e ` t1 : tp2 → tp1 e ` t2 : tp2(TAPP)e ` t1 t2 : tp1
uniﬁcation?

a : int ` (λx : T1 .x) a : T2?
a : int ` λx : T1 .x : tp2 → T2 a : int ` a : tp2
a : int ` (λx : T1 .x) a : T2

¾ substitution?
a : int ` λx : T1 .x : tp2 → T2 a : int ` a : tp2
a : int ` (λx : T1 .x)a : T2
(proof tree after one step)` λa : int.((λx : T1 .x) a) : int → T2
Fig. 3. Applying an inference rule with uniﬁcation

Among the three steps, (1) and (3) are taken care of by Mikiβ. For (2), users
are currently requested to write a uniﬁcation function for the user-deﬁned data.
For example, deﬁne a function deref type that dereferences a metavariable:
let rec deref_type tp = match tp with
MetaType(_, {contents = Some(tp’)}, _) -> deref_type tp’| _ -> tp

Then, the uniﬁcation function for types can be deﬁned as follows:
let rec unify_type tp1 tp2 =match (deref_type tp1, deref_type tp2) with(* case1 : meta type and meta type *)(MetaType(_, op1, _), (MetaType(_, op2, _) as tp2’)) ->if op1 != op2
then op1 := Some(tp2’)(* case2 : meta type and concrete type *)| (MetaType(s, op, _), tp) | (tp, MetaType(s, op, _)) ->if occur s tp (* check if s occurs in tp *)then raise Unify_Error
else op := Some(tp)(* case3 : concrete type and concrete type *)| (Fun(tp1, tp2, _),Fun(tp3, tp4, _)) ->unify_type tp1 tp3; unify_type tp2 tp4| (TVar(tv1, _), TVar(tv2, _)) -> unify_tvar tv1 tv2| _ -> raise Unify_Error
Since uniﬁcation functions have a uniform structure, we expect to generatethem from the data deﬁnition in the future.
3.4

Deﬁnition of Drawing

Since the object layout diﬀers from one system to another, users specify how
data is layout on a display in Mikiβ. For this purpose, Mikiβ oﬀers a few drawing
functions.
– create str : string → id t
To create and layout a string object on a display.
– combineH : id t list → id t
To layout objects horizontally and make them one object.
– combineV : id t → id t → id t
To layout two objects vertically and make them one object. (In case of an
expression which has only horizontal layout, this function is not necessary.)
Using these functions, users specify a drawing function in a way GUI identiﬁers are combined through combineH and combineV. For example, a function
drawing type t data type is as follows:
let rec draw_type tp = match (deref_type tp) with
TVar(tv, _) ->let tv’ = draw_tvar tv inTVar(tv’, get_tvar_id tv’)
| Fun(tp1, tp2, _) ->let tp1’ = draw_type tp1 inlet tp2’ = draw_type tp2 inFun(tp1’,tp2’,
combineH [get_type_id tp1’; create_str " -> ";get_type_id tp2’])| MetaType(str, op , _) -> MetaType(str, op, create_str !str)
3.5

Main and Supporting Functions

Up to here, we have shown how to deﬁne inference rules to be used in Mikiβ.
It is mostly independent of GUI and users of Mikiβ can concentrate on thespeciﬁcation of judgements and inference rules.
To build a GUI system, the deﬁnition of judge t and other helper functions
deﬁned by users are packaged into a module and passed to the tree functor
provided by Mikiβ. The tree functor contains various GUI-related functions,such as:
Function Registration At start up, each function in infer button list is
assigned a button on the display.
Object Selection When a mouse is clicked, the clicked object is searched and
its GUI object identiﬁer is returned. To select a user-deﬁned data, one currently has to specify a fold-like function for the data.
Inference Rule Application When a button is pressed, the selected function(inference rule) is used to grow a proof tree.
Replacing Metavariable Names A name of a metavariable can be changed
consistently by right-clicking a mouse and inserting a new name into a textbox.
Undo Because uniﬁcation is implemented as side-eﬀects, it is not straightforward to undo the inference. Mikiβ supports undo by recording all the userinteraction and redo it from the original judgement.
The complete GUI system is then obtained by linking the tree functor withthe main function that creates an empty window, initializes it, and launches
the event loop. The following diagram shows the overall structure of the GUI
system:'$User’s Deﬁnition
Tree Functor
GUIDeﬁnition of syntax+⇒ GUI
Library ⇒andMain Function
four functions&%→

To use the GUI system, we take the following steps:
1. Enter an expression you want to infer to a text box at the top, and press
the Go button (Fig. 4).
2. Select a target judgement with a mouse click (Fig. 5), and press a button
that you want to apply to the target judgement (Fig. 6). In case the selected
inference rule is inapplicable, nothing will happen.
3. Repeat the second step until the proof tree is complete (Fig. 7).

4

Fig. 4. Enter a judgement

Fig. 5. Select a target judgement

Fig. 6. Apply an inference ruleFig. 7. Inference ﬁnished

ExamplesIn this section, we show several experiences of using Mikiβ.
4.1Type system for shift and reset

The control operators, shift and reset, are introduced by Danvy and Filinski [2]to capture the current continuation up to an enclosing delimiter. Their monomorphic type system is a generalization of the one for lambda calculus and mentions
the answer type of the enclosing context. The judgement has the following form:
Γ; α ` e : τ; βIt reads: under a type environment Γ , a term e has a type τ , and the evaluationof e changes the answer type from α to β. With this type system, the rule forapplication, for example, is as follows:Γ ; γ ` e1 : (σ/α → τ /β); δ Γ ; β ` e2 : σ; γ(app)
Γ ; α ` e1 e2 : τ ; δ
Although conceptually simple, it is extremely hard to keep track of all thesetypes. With Mikiβ, one can simply input all the inference rules and obtain a
GUI system for it that takes care of all the types. We could actually give thedeﬁnition in less than an hour.

4.2

System F

System F adds two inference rules to the simply-typed lambda calculus [5]:Γ, X ` t : T(T-TABS)Γ ` ΛX.t : ∀X.T

Γ ` t : ∀X.T2(T-TAPP)Γ ` t [T1 ] : T2 [X 7→ T1 ]Here, we notice that (T-TAPP) uses a type substitution at conclusion. Itmeans that to use (T-TAPP) to grow a proof tree, we need to unify the type
T2 [X 7→ T1 ] with the type of the current judgement. However, without knowing
the structure of T2 , it is impossible in general to perform uniﬁcation at thisstage. It becomes possible only when T2 is instantiated to a concrete type.
To remedy this situation, we change the inference rules (TAPP) and (T-TAPP)
so that all the leaf judgements have only metavariables as types:Γ ` t1 : T

T = T11 → T12Γ ` t1 t2 : T12

Γ ` t2 : T11(TAPP)

Γ ` t : T T = ∀X.T2(T-TAPP)Γ ` t [T1 ] : T2 [X 7→ T1 ]We introduced a new judgement of the form T1 = T2 . It enables us to defer
uniﬁcation. The new judgement can be written as an axiom in Mikiβ:
type judge_t =Judge of env_t * term_t * type_t * id_t
| Equal of type_t * type_t * id_t(* new judgement *)let t_equal() =let tp = new_type() in (* generate a metavariable *)Axiom(Equal(tp, tp, NEW), NEW)At the time of writing, however, we still have to modify the Mikiβ system itself to accommodate the application of substitutions. We are currently gathering
what operations are needed to express various inference systems.
4.3

Sequent Calculus

It is straightforward to specify the inference rules for sequent calculus. However,judgements in sequent calculus have additional ﬂexibility. For example, in the(∨L) rule below:
Γ, A ` ∆ Σ, B ` Π(∨L)Γ, Σ, A ∨ B ` ∆, Π
formulas in the antecedent (Γ , Σ) and the succedent (∆, Π) are separated at anarbitrary place to obtain the two premises. To support such arbitrary separation,
we had to introduce into Mikiβ a mechanism to insert a cursor in the formulas
and to choose a separation point. Since it is expected that such mechanism isneeded in other systems (such as parsing in the natural language processing),
we hope to support it in Mikiβ in the future.
More generally, we hope to include a general way to incorporate arbitrarily
complex programmable operations into Mikiβ.

5Related Work

Although the goal is quite diﬀerent, visualising proof trees has much in common with theorem proving. Actually, growing a proof tree can be regarded as
decomposing and proving goals in theorem proving. A theorem prover typically
implements various kinds of automation, such as tactics found in Coq [1]. It is
an interesting challenge to incorporate such automation in Mikiβ. It would thenbecome possible to apply (TWEAK) automatically before (TVAR).
Geuvers and Jojgov [4] study incomplete proof trees with metavariables anddiscuss their semantics. Although they do not mention GUI, their result could
be regarded as a theoretical basis of our work.
PLT Redex [3] is a domain speciﬁc language to specify operational semantics.
Given a deﬁnition of operational semantics, PLT Redex oﬀers (among otherfeatures) graphical output of reduction of terms.

6Conclusion and Future WorkIn this paper, we have described Mikiβ, our on-going project to visualize proof
trees. Given deﬁnition for judgements and inference rules, Mikiβ produces a GUI
system for it. Although users are required to write certain amount of deﬁnitionin OCaml, Mikiβ mostly takes care of GUI parts and users can concentrate on
the formalization of inference rules. Our experience of using Mikiβ shows that
it is at least useful to visualize relatively simple systems.
To cope with more complex systems, we still need to enhance GUI partsof Mikiβ. We are currently implementing various systems in Mikiβ to extract
what features we need to specify them in a GUI-independent way. Through thisprocess, we hope to make Mikiβ a more general and useful tool for visualizing
proof trees.

Acknowledgment
We received many useful comments from the anonymous reviewers.

References
1. Yves Bertot and Pierre Castéran, Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions, EATCS Series, Berlin:
Springer (2004).
2. Olivier Danvy, and Andrzej Filinski “A Functional Abstraction of Typed Contexts,” Technical Report 89/12, DIKU, University of Copenhagen (July 1989).
3. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt, Semantics Engineering with PLT Redex, Cambridge: MIT Press (2009).
4. Herman Geuvers and Gueorgui I. Jojgov. “Open Proofs and Open Terms: A Basisfor Interactive Logic,” In Proc. of CSL 2002. LNCS 2471, pp.537–552.
5. Benjamin C. Pierce, Types and Programming Languages, Cambridge: MIT Press(2002).