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 (International)

Refereed Publications (Domestic)

Non-refereed Publications (such as preprints)

Open-Source Software


SATySFiA statically-typed, functional typesetting systemOCaml1.2k80

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.


otfedAn OpenType font format encoder & decoder written in OCamlOCaml17

An OCaml library for encoding/decoding OpenType fonts used as a new font-manipulating backend of SATySFi.


SesterlAn ML-like statically-typed ErlangOCaml1505

A statically-typed Erlang.

A Tian Jiu Pai (天九牌) Game Server

game_tianjiupaiA Tian Jiu Pai (天九牌) game server written in Sesterl & ElmElm151

A Web server where multiple people can play Tian Jiu (Tien Gow, 天九). Implemented in Sesterl and Elm, and can be deployed on an AWS EC2 instance.

APBuf (Algebraic Protocol Buffers)

apbufAlgebraic protocol buffersOCaml13

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.


tex_of_ocamlA compiler for untyped lambda terms to TeX codeTeX5

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.


toy-macro-mlAn implementation of MacroML [Ganz, Sabry & Taha 2001]OCaml301

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


hugo_theme_upcardsA simple card-based Hugo themeJavaScript3

A Hugo theme developed for creating this Web site.

Talks and Presentations


  • Apr 2023 – present (Ph. D. candidate): Course of Communications and Computer Engineering, Department of Informatics, Graduate School of Informatics, Kyoto University
  • Apr 2016 – Sep 2018 (Master): Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo
    • Oct 2017 – Mar 2018: A leave of absense
  • Apr 2012 – Mar 2016 (Bachelor): Department of Mathematical Engineering and Information Physics, Faculty of Engineering, The University of Tokyo