セミナーの内容

定理証明支援系 Coq のチュートリアルです。実際に Coq を使いながら学ぶハンズオン形式です。はじめて Coq に触れる人が対象です。かんたんな論理式の証明からはじめて、証明付きプログラムからコードを抽出できるようになることを目指します。

プログラミングに関わる人が Coq を仕様やプログラムの検証に使うことを想定しています。内容として初等的なものになります。数学や論理学を専門にしている人向けではありません。

セミナーは2日間の構成です。この CONNPASS のイベントに申し込むことで2日間のセミナーに参加できます。

はじめての人にとっては知的好奇心をくすぐる目新しい考え方が次から次へと現れる刺激的なセミナーです。フルに頭を使いますから甘いものを用意してご参加ください。

プログラム

第1日目 7月3日（土）13:00-18:00

• Coq による論理式の証明
• 定義と使用
• 数学的帰納法
• 述語の帰納的定義

第2日目 7月4日（日）13:00-18:00

• Calculus of Inductive Constructions
• 依存型によるプログラミングと検証
• プログラム抽出

※ 進捗によって一部内容とスケジュールを変更する場合があります。

講師について

株式会社 PRINCIPIA 代表取締役 初谷 久史

CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師

必要な知識

• 高校で習う程度の数学の知識：命題と論理，数学的帰納法
• 関数型プログラミングの初等的な知識：関数適用，抽象（λ式，無名関数），再帰，代数的データ型，パターンマッチ

必要なもの

• 定理証明支援系 Coq （CoqIDE という統合環境を基本に解説します）

配布物と Zoom meeting URL

セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。

同じメッセージを複数回送信する場合があります。あらかじめご了承ください。

注意事項

• 配布資料の公開は禁止です。
• 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
• 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。