証明駆動競技プログラミング: セグメント木ライブラリの検証

水野 雅之@fetburner2026年7月12日Track B25 分

Rocqで競技プログラミング向けセグメント木を検証。要素数が2の冪でない配列埋め込み実装を題材に、泥臭い最適化コードを証明する方法論が分かる。

発表概要の全文は fortee の発表ページ で読めます。