Leanで正規表現エンジンをつくる。そして正しさを証明する

対象とする聴衆のレベル（該当するレベルを記載してください。）

• Beginner: 分野の前提知識を必要としない
• Intermediate: 分野の基礎知識を持っている

セッションのテーマ（該当するテーマを記載してください。なければ追加頂いて良いです）

• 導入事例
• 言語処理系（コンパイラー、インタープリターなど）
• Tips

セッションの概要

このセッションでは、Leanの二面性—定理証明支援系としての強力な検証能力と、依存型を備えた純粋関数型プログラミング言語としての実践性—を活かし、正規表現エンジンの実装とその正しさの検証に取り組んだ経験を紹介します。

Leanが純粋関数型言語として持つ特徴を紹介し、特に配列に対する破壊的変更（！）のサポートに注目します。この仕組みを活かすことで、オートマトンベースの正規表現エンジンを効率的に実装できることを説明します。

次に、正規表現エンジンの実装の正しさを検証する過程で直面した具体的な課題、たとえば正規表現の仕様自体の曖昧さや証明の再利用をどのように解決したかを実例を交えて掘り下げます。通常のソフトウェア開発のようにモジュール化で対処したケースもあれば、定理証明支援系ならではの問題とその解決法など、さまざまな例を紹介します。

その他にも、依存型の利用についてもお話しします。依存型は型システムの強力さを一段引き上げますが、一方で型システムに対して人工的な制限も追加してしまいます。ある意味で諸刃の剣である依存型に対して、どのような場面で使うのが良いのか、どのような場面では避けた方が良いのかを例を挙げて説明します。

これらのトピックを通じて、依存型を利用した開発や定理証明がどのようなものであるのかを皆さんに知っていただけたら幸いです。そして、興味をもったらぜひ挑戦してみてください。みんなも定理証明、しよう！