定理証明支援系 Coq チュートリアル

イベント内容

セミナーの内容

定理証明支援系 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 開発者

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

必要な知識

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

必要なもの

配布物と Zoom meeting URL

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

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

注意事項

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

連絡先

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

注意事項

※ こちらのイベント情報は、外部サイトから取得した情報を掲載しています。
※ 掲載タイミングや更新頻度によっては、情報提供元ページの内容と差異が発生しますので予めご了承ください。
※ 最新情報の確認や参加申込手続き、イベントに関するお問い合わせ等は情報提供元ページにてお願いします。

類似しているイベント