ウォンテッドリーのインフラエンジニアの水野です。7月11日から12日まで開催された関数型まつり2026において、実世界で使われているものに近いプログラムに対して形式検証を適用する発表を行いました。
証明駆動競技プログラミング: セグメント木ライブラリの検証
当日の発表スライドは Speaker Deck で公開しています。
関数型まつり2026で行った発表について
発表内容の詳細
関数型まつり2026で行った発表内容を説明すると、実世界で使われるプログラムに対して形式検証を適用しようとした際に生じる困難について、ソフトウェア工学的な考え方を用いて解決を図るものです。
テスト駆動開発で網羅できるケースには限界があるので定理証明支援系等を用いた形式手法によって仕様を満たしていることを数学的に保証したくなりますが、本当に検証すべき実社会で使われているプログラムは性能上の要請から形式検証を行いやすい綺麗な形はしていないため、直接的な検証は困難が伴います。そこで、ソフトウェア工学的な工夫によってプログラムを数学的に扱いにくくしている要因を解きほぐすことで、形式検証の適用が容易になることをデモンストレーションしました。
発表で題材とした、競技プログラム等で用いられるセグメント木ライブラリの形式検証については昔ブログに書いていた一連の記事が下敷きになっています。詳細が気になる方はこちらもどうぞ。
- セグメント木の形式的検証
- セグメント木の一次元配列による実装の検証
- 形式的に検証したセグメント木の実装を使って競技プログラミングの問題を解く
- 要素数が2の冪でないセグメント木でも，再帰を使わずに二分探索できる
ブログ記事の中にもリンクがありますが、セグメント木ライブラリの検証に用いた Rocq の実装は Gist にアップロードされています。
完全二分木に限らない、セグ木の配列への埋め込み
また、発表中で軽く触れた二分探索の検証についても昔ブログ記事で書いているので、そちらも良ければ参考にして下さい。
登壇の振り返り
50枚のスライドを25分で駆け抜ける構成にしたのですが、当日は少し時間が不足気味で終盤がやや駆け足になってしまいました。もう少し発表練習を行うか話す内容を絞るべきでしたね。
質疑では「今回検証したセグメント木ライブラリは AtCoder の問題を解くことでベンチマークを行っていたが、同じ問題を C++ で解くとどれぐらいの実行時間になるか？」といった趣旨の質問があり、「覚えていないが C++ の実行時間は OCaml の大体三分の一程度になるので 50ms 位だと思う」といった内容で回答しましたが、後で確認してみたら概ねその通りになっていたようで良かったです。
Sign In - AtCoder
発表中には初日に印象的な発表をされていた konn さんや去年運営スタッフをされていたよんたさんが X 上で実況をして下さっていて、感触が良さそうだったのも嬉しかったです。proof ninja の yoshihiro503 さんにも発表前に声をかけて頂けましたが、やはりやった事が人に見て貰えている実感を持てるのはオフラインイベントの良い所ですね。
参加レポートを書いて下さった方にも発表に触れて頂けて、大変励みになりました。
人生初のカンファレンスに参加してみた感想（関数型まつり 2026） - Qiita
印象に残ったセッション
気になる発表の時間が被っていたり、発表準備のために会場を移れなかったりして涙を飲む場面が多かったのですが、興味深いセッションが多く有意義な時間になりました。印象に残ったものを挙げるとしたら次の通りです。
OCaml で作ったアプリを実運用している
OCamlで作ったアプリを実運用している
最近非常に勢いのある OCaml ですが、実際のプロダクトで使われている話は Jane Street 等海外の限られた事例しか聞かなかったので、国内の貴重な事例を知れて興味深かったです。いつか業務で OCaml とか Rocq とか（はたまた SML# とか）を使えたら楽しそうですね…
発表中で OCaml Meeting 2026 in Tokyo の存在を知ったのですが、どうも枠が既に埋まっているようで残念でした。
本物のプログラマーは unsafe と型システムを使う
本物のプログラマーは unsafe と型システムを使う 〜拡張可能レコードを作って学ぶ黒魔術入門〜
Haskell での拡張可能レコードの実装を題材として、実用上求められる unsafe なエスケープハッチとの向き合い方についての発表でしたが、理論的な綺麗さと実用上のパフォーマンスとの折り合いをどう付けるかという点で僕の発表と共通するものがあり興味深かったです。型パズルやるのは良いけど性能の出ないデータ構造を採用しては本末転倒なんですよね。
「弱い」世界から分解する「データ型」の概念
「弱い」世界から分解する「データ型」の概念
fold と unfold を両方入れると停止しなくなるという話は「そうだろうな」と思いながら聴いていたのですが、そこから余帰納的データ構造の話が展開されて驚きました。雰囲気で余帰納的データ構造や余帰納法を使ってしまっているので、ちゃんと勉強しないと駄目ですね…
2026 年に読む “The Definition of Standard ML” 〜 現代の堅牢なソフトウェア設計の源流として
2026 年に読む "The Definition of Standard ML" 〜 現代の堅牢なソフトウェア設計の源流として
Standard ML を題材としてプログラミング言語のセマンティクスがどのように形式的に定義されているかを紹介する発表でしたが、The Definition of Standard ML は僕も少し読んだ事があったので懐かしい気持ちになれました。
実は昨年の関数型まつりには SML# の大堀先生や上野先生が参加されていて Standard ML 界隈に大変な勢いを感じたのですが、今年は SML 関連の発表がこの1本だけで少し寂しくもありました。来年はまた盛り上げていきましょう。
多段階計算によるコンパイル時テンソル形状検査
多段階計算によるコンパイル時テンソル形状検査
テンソルの形状の静的検証というと型レベル自然数を使った手法が古くから知られていますが、多段階計算を用いると実用上優れた体系を作れるという発想が面白かったです。やはり実際のソフトウェアを開発する上では理論的に綺麗なだけでは駄目で現実との折り合いを付ける必要がある訳ですが、ここで扱っている体系は良い落とし所を探っていると感じました。聞けば国際会議で発表された内容が基になっているそうで、こんな贅沢な発表を国内で聴けて良いのでしょうか…！
まとめ
登壇者としても聴衆としても実り多い2日間でした。運営スタッフの皆さん、発表を聴いてくださった皆さん、会場で話してくださった皆さん、ありがとうございました。この素敵なイベントが末長く続いていくように、コミュニティに貢献していきたいです。
/assets/images/7052304/original/49100b17-5866-4cec-b50b-a37ea73565e9?1638782149)
/assets/images/7052304/original/49100b17-5866-4cec-b50b-a37ea73565e9?1638782149)
/assets/images/7053725/original/28d1b135-13b4-4f46-895f-d5f5fb5ae243?1624246858)
