MaruLabo ハンズオン「はじめてのCoq」
正確にいうと、Coqは単なる言語ではなく、「形式的証明管理システム」と呼ぶべきものです。
Coqは、次のことを可能にします。
- Coqを用いて、プログラムの対象や数学の対象を定義できます。
- Coqを用いて、プログラムの意味や仕様、また、数学の定理を記述できます。
- Coqを用いて、インタラクティブに、これらの仕様や定理に形式的証明を与えることができます。
- Coqは、与えられた証明が正しいか否かを、簡単にチェックすることができます。
それだけではありません。ソフトウェア・エンジニアリングの基礎であるソフトウェア科学の世界でも、Coqを用いてデータ構造やアルゴリズムを再定義し、ソフトウェア科学の教育のスタイルを一新しようという動きが広がっています。Coqは、ソフトウェア科学の"Lingua Franca (普遍言語)" としての地位を確立しつつあります。
今回のハンズオンは、はじめてCoqに触れる人を対象にした、おそらく「はじめての」ハンズオンです。
Coqの学習には、率直に言って難しさがあります。これまでも「新しい言語」を学ぶことを経験してきた人は多いとと思います。そこでは、Cを知っていればJavaの学習の助けになりましたし、Rubyを使っていればPythonは入りやすく感じた経験はあると思います。ただ、Coqに関して言えば、これまでの言語経験は、あまり助けにならないのです。逆に言えば、みな同じ出発点で新しいシステムを学ぶと思ってもらえばいいと思います。
また、Coqの勉強をはじめて「覚えるべきこと」が多いことに困惑するかもしれません。これも、ある程度は我慢してもらうしかないのです。ただ、基本的なパターンを習得すれば、定型的なイデオムがあることがだんだん分かってきます。
少し乱暴な言い方をすれば、本を読んでCoqを学ぶことは、むしろ難しいのです。Coqに何かを入力すると、Coqが反応を返す。その反応を見て次の入力を考える。そうしたインタラクティブな人間とCoqのやりとりこそが、Coqプログラミングの真骨頂なのです。そうした経験は、本を読むだけでは得られません。繰り返し課題を解いて、試行錯誤でCoqと対話するハンズオンの経験は、Coqを学ぶ上で大きなステップになると確信しています。
今回のハンズオンは、次のような特徴を持っています。
- Coqのシステムは、あらかじめ主催者がクラウド上にインストールしておきます。受講者は、ブラウザーが使えるマシンを持参するだけで、すぐにCoqプログラミングの学習がはじめられます。
- ハンズオンでは、講義と演習のサイクルを繰り返します。
- ハンズオン資料の配布は、ブラウザー上のjupyter notebookを通じて行います。この資料は、Coqとのインタラクティブな会話の舞台になる「動く資料」です。受講者の入力に対するCoqの反応は、ブラウザー上ですぐに確認できます。
- ハンズオンの獲得目標は、Coqでの基本的な「証明スキル」を身に付けることに置かれています。
- そのために、沢山の演習問題を解いてもらいます。
皆さんの参加をお待ちしています。
【参考資料】
- 「プログラムと論理」https://www.marulabo.net/docs/programlogic/
- 「ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界」https://www.marulabo.net/docs/deep-spec/
- 「型の理論入門」https://www.marulabo.net/docs/type-theory-2/
- 「Yet Another AI -- RPAは「推論エンジン」の夢を見るか」https://www.marulabo.net/docs/yet-another-ai/
Updates
- イベント詳細情報を更新しました。 Diff#485988 2019-10-21 05:44:04
Sat Nov 9, 2019
1:00 PM - 7:00 PM JST
1:00 PM - 7:00 PM JST
Add to Calendar
- Venue
- Tickets
-
一般 SOLD OUT ¥12,000 マルレク個人協賛会員 SOLD OUT ¥8,000 丸山レクチャーズ会員 SOLD OUT ¥8,000 丸山レクチャーズ特別会員 SOLD OUT ¥5,000 学生 SOLD OUT ¥3,000
- Venue Address
- 目黒区大橋２丁目２２−４２ 地下1階 Japan
- Organizer
-
マルレク＋MaruLabo1,206 Followers
