著者情報

Contact

興味

  • プログラミング言語理論
    • 型理論，プログラム意味論
    • プログラム検証，形式手法，モデル検査
    • メタプログラミング，多段階計算，マクロ機構
    • 並行計算
  • タイポグラフィ関連技術
    • 組版処理アルゴリズム，フォントフォーマット
  • レタリング，タイプデザイン

査読つき論文（国際）

査読つき論文（国内）

査読なし論文（preprint等）

オープンソースソフトウェア

SATySFi

SATySFiA statically-typed, functional typesetting systemOCaml1.2k84

組版処理システム．TeX/LaTeXと似た形態のソフトウェアですが，静的型つきのいわゆる函数型言語が搭載されており，その言語によってライブラリや文書の一部を記述でき，不整合があれば型検査により素早く比較的わかりやすい形で報告してくれるのが特長です．

本ソフトウェアは2017年度IPA未踏IT人材発掘・育成事業の1プロジェクトとして採択され，成果により著者がスーパークリエータに認定されました．

Otfed

otfedAn OpenType font format encoder & decoder written in OCamlOCaml18

OpenTypeフォントフォーマットのエンコードとデコードを行なうOCaml製ライブラリ．SATySFiのフォントを扱うバックエンドとして使用しています．

Sesterl

SesterlAn ML-like statically-typed ErlangOCaml1525

Erlangに静的に型をつけてラップした言語．

天九ゲームサーバ

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

SesterlとElmで実装した，天九というテーブルゲームのオンライン対戦サーバ．Webサーバとしては問題なく動作しますが，まだ運用のための調整を必要とし，リリースまで至っていません．

APBuf (Algebraic Protocol Buffers)

apbufAlgebraic protocol buffersOCaml13

Protocol Buffersとよく似た目的のツールで，フォーマット定義を記述するとそのエンコーダとデコーダを生成する処理系です．多相型や代数的データ型をネイティブでサポートしているのが特長です．エンコーダとデコーダのターゲット言語としてはScala，Elm，Sesterlに対応しています．

tex_of_ocaml

tex_of_ocamlA compiler for untyped lambda terms to TeX codeTeX5

OCaml風の構文で書かれた値呼び型なしλ計算のプログラムを，TeX言語上で \edef により完全展開できるコードへとコンパイルしてくれるコンパイラ．

toy-macro-ml

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

MacroML [Ganz, Sabry & Taha 2001] という，多段階計算をベースとするマクロシステムを実装した小さいコンパイラ・インタプリタです．

Upcards

hugo_theme_upcardsA simple card-based Hugo themeJavaScript3

このWebサイトを制作するために作成したHugoテーマです．

発表等

Education

  • 2023年4月– 京都大学大学院 情報学研究科 情報学専攻 通信情報システムコース
  • 2016年4月–2018年9月 東京大学大学院 情報理工学系研究科 コンピュータ科学専攻
    • 2017年10月–2018年3月 休学期間
  • 2014年4月–2016年3月 東京大学 工学部 計数工学科 数理情報工学コース
  • 2012年4月–2014年3月 東京大学 教養学部 理科1類
  • 2009年4月–2012年3月 灘高等学校
  • 2006年4月–2009年3月 灘中学校

受賞等

スキルセット等

比較的得意，またはよく経験している分野

  • 言語処理系：
    • 言語処理系の実装を何度も行なっており，とりわけ型システムを設計して型検査器を作り込むのが好きです．
  • タイポグラフィ関連技術：
    • SATySFiやotfedの実装に活かすためにPDFファイルのフォーマットやOpenTypeフォントのフォーマットについて仕様書を精読したことがあり，広範に亘って把握しています．
  • Webバックエンド：
    • 業務としてバックエンドの開発に3年半ほど携わった経験があるほか，趣味でもバックエンドの実装をよくします．
    • 趣味でWebSocketにより双方向に通信するゲームサーバを設計・実装したことがあります．
  • 映像配信技術・メディア技術：
    • RTMPやHLSの仕様を把握しており，実際にRTMPサーバやHLSサーバの実装をいじったりしています．
    • 配信システムとしてどのような役割のサーバ群をどう配置すればパフォーマンス上よいかなどについておおよそ把握しています．
    • ISOBMFFのフォーマット，符号化の仕組みなどについても一定程度把握しています．
    • WebRTCについてはまだ特に馴染みはありません．

その他の経験

  • Webフロントエンド：
    • 業務経験はありませんが，趣味でよく触っています．ECMAScriptやCSSの仕様について熟知しているほどではありませんが，趣味開発でつくりたいものをつくるのにはそれほど苦労しない程度に把握しています．
  • クラウド関連技術：
    • 趣味でAWS上にオンラインゲームのWebサーバを構築し試用で稼働させたりしたことがあります．実運用は未経験です．
  • RDBMS：
    • リレーションの定式化についての理論（正規化など）や，RDBMSの内部実装（インデックスの張り方，B+木，トランザクション処理の戦略など）について一定程度把握しています．ただし，実システムでRDBを利用したり，RDBMS自体をいじったりする機会は，これまでなかなかありませんでした．

実用経験のあるプログラミング言語

そもそもプログラミング言語という概念自体が好きなこともあり，大抵の言語は必要になれば身につけられると思いますが，一応各言語にどの程度現状で慣れているかの目安を掲げておきます：

  • OCaml： ★★★
    • 最も流暢に読み書きできる言語です．おそらく延べ20万〜30万行ほど書いているほか，多少処理系の実装を読んだりした経験があります．個人的な心象としても最も好きな言語です．
  • Erlang： ★★★
    • 次いで流暢な言語です．おそらく延べ数万行ほど書いています．業務で2年半ほどの使用経験があるほか，趣味開発でも多少使用します．Erlang VMの仕様や，OTP（≒標準ライブラリ）の実装を読んだりしたことがあります．並行処理用の言語として，OTPも含めて面白くかつ有用な定式化の言語だと思います．とりわけ分散環境が簡潔に構築できるのはこの言語の大きな強みだと感じます．一方で，健全性を満たす型システムが存在しないため，大規模な用途に積極的に使用したいとまでは思っていません．Erlangに型をつけたいという動機で開発中である上記のSesterl参照．
  • Elm： ★★★
    • 趣味開発で使用経験があります．おそらく延べ1万行ほど書いていると思います．
  • Haskell： ★★☆
    • 業務で最もよく使っているほか，趣味や研究上の実装でも或る程度使っています．抽象化能力の高さがかえって仇して書いた人以外が読解に手間取るコードになってしまうこともしばしばですが，全体的にとても快適な使用感を覚えています．
  • TypeScript： ★★☆
    • 業務で専らReactと共にフロントエンドの実装に使っています．path-sensitiveな型システムにしばしば驚かされます．
  • Rust： ★★☆
    • 趣味で多少書くほか，業務でも半年程度の使用経験があります．とても面白い型システムをもつ言語だと感じていますが，型エラーが出たときにどう修正すればよいか自分にとってすぐにはわからないことも多く，所感としてはまだまだ使いこなせていない段階です．
  • Go： ★★☆
    • 業務でのみ，半年程度使用した経験があります．既にgenericsが導入されたようですが，genericsのない時代に触っていました．代数的データ型やgenericsの仕組みがないことをネックに感じましたが，あえて抽象化機構を提供しないことで誰が書いても似たコードになり読みやすいのは利点かもしれないという気づきも得ました．また，標準ライブラリと周辺ツールがとても成熟しているのは魅力だと思います．
  • Scala (2.x)： ★★☆
    • 主に趣味開発で使用経験があります．おそらく延べ数千行ほど書いていると思います．
  • C言語： ★★☆
    • 主に学部生の頃にアルゴリズム理解のために書いていました．厳密な言語仕様などは把握しきれていませんが，大きな支障なく書くことは可能です．
  • Emacs Lisp： ★☆☆
    • メジャーモードを定義するEmacsの小規模なパッケージを定義する際に何度か書きました．
  • Python (3.x)： ★☆☆
    • それほど積極的には用いておらず，標準的な函数を記憶していないため調べながら書くことになります．業務でシェルスクリプトの代替として使用したり，matplotlib によって分析・可視化などに使用したりしたことがある程度です．参照渡しなのか値渡しなのかなどがわかりづらい，健全性を満たす型システムをもたないなどの理由で正直なところあまり好みではない言語です．
  • Ruby： ★☆☆
    • それほど多くの利用経験はありません．学部生の頃に演習で書いていたのがほとんどです．SATySFiの開発に一時期利用していました（他の方からcontributionで頂いた実装を拡張するために読み書きしていました）．

基礎的リテラシー

  • CI/CD：
    • 趣味では主にGitHub Actions，業務では主にJenkinsを使用し，ビルドパイプラインの構築・改善経験あり．
  • アルゴリズム：
    • 競技プログラミングなどの習慣は現状ないため瞬発力があるわけではありませんが，学部で習得する程度の典型的アルゴリズムについては把握しています．
    • 学部生の頃は組合せ最適化などが専門分野でした．
  • 暗号・認証・セキュリティ
    • 公開鍵暗号や署名の仕組みについての基礎的な理解が一定程度あります．
    • XSS，CSRFといった基本的なWebセキュリティ上の事象や，同一生成元ポリシーといった対策用の概念について把握しています．