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
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
Higher-Order Program Verification via HFL Model Checking.
In Proceedings of ESOP 2018
Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada and Naoki Kobayashi:
Automatically Disproving Fair Termination of Higher-Order Functional Programs.
In Proceedings of ICFP 2016
For more details of my academic activities, please see this page.
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.