研究部 個人活動実績

N高11期生
研究部六期生

基本的に低レイヤー、形式検証関係の分野での研究をしている。

今やっているのはSailやXedからLeanへISA定義をトランスパイルして色々なアーキテクチャに対応しているISAバックエンドを自動生成する物の開発、またそれを使ってTCBを極限まで小さくした形式検証のプログラミング言語を作ってます。

Curry-Howard対応とか型理論だとか帰納的不変性だとか数理論理学とかとか、小難しいことをやっているけどもマージで数学は分からんのです。

最近時間が経つのが早すぎるので老けたかな？と心配している今日この頃。
何に使うかわからないコード片はたまに量産する。