Keiichi Watanabe

A software engineer who loves programming languages.
Interests: Programming languages, Program verification, Type theory, Functinal programming


  • Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi:
    Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking.
    In Proceedings of PEPM 2019 [Paper]
  • Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
    Higher-Order Program Verification via HFL Model Checking.
    In Proceedings of ESOP 2018 [arXiv]
  • Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada and Naoki Kobayashi:
    Automatically Disproving Fair Termination of Higher-Order Functional Programs.
    In Proceedings of ICFP 2016 [Paper]

For more details of my academic activities, please see this page.


constexpr-8cc: Compile-time C Compiler

constexpr-8cc is a C compiler implemented as C++14 constant expressions. So you can compile while you compile! This is a joke compiler, but shows how powerful compile-time computations in C++ are!

UCC: C Compiler written in OCaml

UCC is an almost C89 compatible compiler written in OCaml. The target architecture of UCC is GAIA, which was designed in undergraduate experiments at the University of Tokyo in 2014. By using UCC, we succeeded to compile and run xv6, a simple Unix-like OS.

GitBucket-Fess-Plugin: GitBucket Plug-in for Cross-Repository Search

This is a GitBucket plug-in that provides multiple-repositories search. This plug-in works with a full-text search server Fess.