About the Author



  • Theory of programming languages
    • Type theory, semantics of programming languages, etc.
    • Program verification, formal methods, model checking, etc.
    • Metaprogramming, multi-stage programming, macro systems, etc.
    • Concurrency
  • Engineering for typography
    • Typesetting algorithm, font formats, etc.
  • Lettering and type design

Refereed Publications

Open-Source Softwares


A typesetting system equipped with an OCaml-like statically-typed functional language in which one can implement libraries or write some part of documents. The strongest point of SATySFi is typically quick and informative type error reports, which help you write documents or libraries with ease and efficiency.


An OCaml library for encoding/decoding OpenType fonts. Intended to be used as a new back end for SATySFi in the future.


A statically-typed Erlang.

A Tian Jiu Pai (天九牌) Game Server

A Web server where multiple people can play Tian Jiu (Tien Gow, 天九). Implemented in Sesterl and Elm.

APBuf (Algebraic Protocol Buffers)

APBuf is a tool having a purpose similar to that of Protocol Buffers, but it is characteristic in that it natively supports ADTs and parametric polymorphism.


A compiler that transforms programs of a call-by-value untyped lambda calculus (written in an OCaml-like syntax) into TeX code expandable by \edef. The compiler is implemented in Rust.


An implementation of MacroML [Ganz, Sabry & Taha 2001], a macro system based on the multi-stage programming.


A Hugo theme developed for creating this Web site.