目次
Contact
- GitHub:
@gfngfn
- Twitter:
@bd_gfngfn
,@en_gfngfn
興味
- プログラミング言語理論
- 型理論,プログラム意味論
- プログラム検証,形式手法,モデル検査
- メタプログラミング,多段階計算,マクロ機構
- 並行計算
- タイポグラフィ関連技術
- 組版処理アルゴリズム,フォントフォーマット
- レタリング,タイプデザイン
査読つき論文
- 諏訪 敬之.複数ステージの値が同一ストラクチャのメンバとして共存できる多段階計算のためのモジュールシステム.第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022), 2022.
- Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi and Atsushi Igarashi. Verification of code generators via higher-order model checking. In Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM ’17). pp. 59–70, 2017.
オープンソースソフトウェア
SATySFi
組版処理システム.TeX/LaTeXと似た形態のソフトウェアですが,静的型つきのいわゆる函数型言語が搭載されており,その言語によってライブラリや文書の一部を記述でき,不整合があれば型検査により素早く比較的わかりやすい形で報告してくれるのが特長です.
本ソフトウェアは2017年度IPA未踏IT人材発掘・育成事業の1プロジェクトとして採択され,成果により著者がスーパークリエータに認定されました.
otfed
OpenTypeフォントフォーマットのエンコードとデコードを行なうOCaml製ライブラリ.将来的にSATySFiのバックエンドとして使用することを企図しています.
Sesterl
Erlangに静的に型をつけてラップした言語.
天九ゲームサーバ
SesterlとElmで実装した,天九というテーブルゲームのオンライン対戦サーバ.Webサーバとしては問題なく動作しますが,まだ運用のための調整を必要とし,リリースまで至っていません.
APBuf (Algebraic Protocol Buffers)
Protocol Buffersとよく似た目的のツールで,フォーマット定義を記述するとそのエンコーダとデコーダを生成する処理系です.多相型や代数的データ型をネイティブでサポートしているのが特長です.エンコーダとデコーダのターゲット言語としてはScala,Elm,Sesterlに対応しています.
tex_of_ocaml
OCaml風の構文で書かれた値呼び型なしλ計算のプログラムを,TeX言語上で \edef
により完全展開できるコードへとコンパイルしてくれるコンパイラ.
toy-macro-ml
MacroML [Ganz, Sabry & Taha 2001] という,多段階計算をベースとするマクロシステムを実装した小さいコンパイラ・インタプリタです.
Upcards
このWebサイトを制作するために作成したHugoテーマです.
発表等
- 諏訪 敬之.招待講演: 静的型つき函数型組版処理システムSATySFiの紹介.第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022),2022.
- Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi and Atsushi Igarashi. Verification of code generators via higher-order model checking. 第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017), 2017.
- 平井 広志,諏訪 敬之.推論システムによるマトロイドの表現について.日本応用数理学会 第12回 研究部会連合発表会,2016.
Education
- 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月 灘中学校
受賞等
- 第1回 日本地学オリンピック 優秀賞
- 第2回 日本地学オリンピック 優秀賞
- 2017年度IPA未踏人材発掘・育成事業 スーパークリエータ
- 2021年 第36回 山内奨励賞
- PPL 2022 発表賞(一般の部)
スキルセット等
比較的得意,またはよく経験している分野
- 言語処理系:
- 言語処理系の実装を何度も行なっており,とりわけ型システムを設計して型検査器を作り込むのが好きです.
- タイポグラフィ関連技術:
- Webバックエンド:
- 業務としてバックエンドの開発に携わっているほか,趣味でもバックエンドの実装をよくします.
- 趣味でWebSocketにより双方向に通信するゲームサーバを設計・実装したことがあります.
- 映像配信技術・メディア技術:
- RTMPやHLSの仕様を把握しており,実際にRTMPサーバやHLSサーバの実装をいじったりしています.
- 配信システムとしてどのような役割のサーバ群をどう配置すればパフォーマンス上よいかなどについておおよそ把握しています.
- ただし,WebRTCについてはまだ特に馴染みはありません.
- ISOBMFFのフォーマット,符号化の仕組みなどについても一定程度把握しています.
その他の経験
- Webフロントエンド:
- 業務経験はありませんが,趣味でよく触っています.
- ECMAScriptやCSSの仕様について熟知しているほどではありませんが,趣味開発でつくりたいものをつくるのにはそれほど苦労しない程度に把握しています.
- クラウド関連技術:
- 趣味でAWS上にオンラインゲームのWebサーバを構築し試用で稼働させたりしたことがあります.実運用は未経験です.
- RDBMS:
- リレーションの定式化についての理論(正規化など)や,RDBMSの内部実装(インデックスの張り方,B+木,トランザクション処理の戦略など)について一定程度把握しています.
- ただし,実システムでRDBを利用したり,RDBMS自体をいじったりする機会は,これまでなかなかありませんでした.
実用経験のあるプログラミング言語
そもそもプログラミング言語という概念自体が好きなこともあり,大抵の言語は必要になれば身につけられますが,一応各言語にどの程度現状で慣れているかの目安を掲げておきます:
- OCaml: ★★★
- 最も流暢に読み書きできる言語です.おそらく延べ20万〜30万行ほど書いているほか,多少処理系の実装を読んだりした経験があります.個人的な心象としても最も好きな言語です.
- Erlang: ★★★
- 次いで流暢な言語です.おそらく延べ数万行ほど書いています.業務で2年半ほどの使用経験があるほか,趣味開発でも多少使用します.Erlang VMの仕様や,OTP(≒標準ライブラリ)の実装を読んだりしたことがあります.並行処理用の言語として,OTPも含めて面白くかつ有用な定式化の言語だと思います.とりわけ分散環境が簡潔に構築できるのはこの言語の大きな強みだと感じます.一方で,健全性を満たす型システムが存在しないため,大規模な用途に積極的に使用したいとまでは思っていません.Erlangに型をつけたいという動機で開発中である上記のSesterl参照.
- Elm: ★★★
- 趣味開発で使用経験があります.おそらく延べ1万行ほど書いていると思います.
- Rust: ★★☆
- 趣味で多少書くほか,業務でも半年程度の使用経験があります.とても面白い型システムをもつ言語だと感じていますが,型エラーが出たときにどう修正すればよいか自分にとってすぐにはわからないことも多く,所感としてはまだまだ使いこなせていない段階です.
- Go: ★★☆
- 業務でのみ,半年程度使用した経験があります.既にgenericsが導入されたようですが,genericsのない時代に触っていました.代数的データ型やgenericsの仕組みがないことをネックに感じましたが,あえて抽象化機構を提供しないことで誰が書いても似たコードになり読みやすいのは利点かもしれないという気づきも得ました.また,標準ライブラリと周辺ツールがとても成熟しているのは魅力だと思います.
- Scala (2.x): ★★☆
- 主に趣味開発で使用経験があります.おそらく延べ数千行ほど書いていると思います.
- Haskell: ★★☆
- 趣味で少しだけ使ったことがあります.必要呼びの評価戦略を活かした使い方はあまりしていません.
- C言語: ★★☆
- 主に学部生の頃にアルゴリズム理解のために書いていました.厳密な言語仕様などは把握しきれていませんが,大きな支障なく書くことは可能です.
- Emacs Lisp: ★☆☆
- メジャーモードを定義するEmacsの小規模なパッケージを定義する際に何度か書きました.
- Python (3.x): ★☆☆
- それほど積極的には用いておらず,標準的な函数を記憶していないため調べながら書くことになります.業務でシェルスクリプトの代替として使用したり,
matplotlib
によって分析・可視化などに使用したりしたことがある程度です.参照渡しなのか値渡しなのかなどがわかりづらい,健全性を満たす型システムをもたないなどの理由で正直なところあまり好みではない言語です.
- それほど積極的には用いておらず,標準的な函数を記憶していないため調べながら書くことになります.業務でシェルスクリプトの代替として使用したり,
- Ruby: ★☆☆
- それほど多くの利用経験はありません.学部生の頃に演習で書いていたのがほとんどです.SATySFiの開発に一時期利用していました(他の方からcontributionで頂いた実装を拡張するために読み書きする必要がありました).
- TypeScript: ★☆☆
- 2015年頃に数千行ほど書いたことがありますが,近年は書いていません.当時と2022年現在とでは全く違う言語になっているだろうと思います.
基礎的リテラシー
- CI/CD:
- 趣味では主にGitHub Actions,業務では主にJenkinsを使用しており,ビルドパイプラインの構築・改善経験あり.
- アルゴリズム:
- 競技プログラミングなどの習慣は現状ないため瞬発力があるわけではありませんが,学部で習得する程度の典型的アルゴリズムについては把握しています.
- 学部生の頃は組合せ最適化などが専門分野でした.
- 暗号・認証・セキュリティ
- 公開鍵暗号や署名の仕組みについての基礎的な理解が一定程度あります.
- XSS,CSRFといった基本的なWebセキュリティ上の事象や,同一生成元ポリシーといった対策用の概念について把握しています.