SF読み進捗ダメです会議 #23 #readcoqart #Coq

イベント内容

証明器Coqの解説書 Coq'Art を読む読書会だったのですが、まずは ソフトウェアの基礎 を読むことになりました。しばらくは本を購入する必要はありません。Webで公開されている資料を使って勉強を進めます。

主催者は証明器についてまったくの素人なので、基本からしっかり勉強する読書会にしようと思っています。「Coqって何？」という方は以下のリンクが参考になるかもしれません。

• プログラミング Coq
• ソフトウェアの基礎 1.0.2
• Coq Tutorial at Proof Summit 2011

Equiv_J: プログラムの同値性
宿題割当てについての一般的アドバイス	@khibino
振る舞い同値性	@khibino
振る舞い同地の性質	@khibino
ケーススタディ: 定数畳み込み	@khibino
プログラムが同値でないことを証明する	@khibino
外延性を使わずに行なう (Optional	@khibino
さらなる練習問題	@khibino
ImpList_J: Imp のリスト拡張
リストを持つ Imp プログラム	練習問題無し
Hoare_J: ホーア論理
ホーア論理
表明	@saka_bar
ホーアの三つ組	@saka_bar
最弱事前条件	@saka_bar
証明規則	@saka_bar
ホーア論理によるプログラムについての推論	@nagaet
修飾付きプログラムの形式化	未定
Rel_J:関係の性質
関係の基本性質	@khibino
反射推移閉包	@khibino
Smallstep_J: スモールステップ操作的意味論
おもちゃの言語	@nagaet
マルチステップ簡約、正規形再び	@saka_bar
ビッグステップ、さらなる練習問題	@khibino
スモールステップ Imp、並列実行 Imp	未定2
Types: さらに自動化	@yugawara
型付きの算術式、構文〜型の健全性	@eldesh
追加演習	未定3

読む順番は 章の依存関係の中心的な章 の矢印を追い掛けます。

スケジュール

開始時間が14時に変更になっています

• 14:00-18:00 ソフトウェアの基礎 の担当部分を発表 or 各自証明
• 18:30-20:00 懇親会(有志)

持ち物

• Coq をインストールしたノートPC (ハンズオンを行なうので必ず持ってきてください！) [https://github.com/sfja/sfja] を自分のノートPCにgit cloneしておいてください
• 全てが型付けされた世界を泳ぐ純粋な心

集合場所

歌舞伎座タワー 21F セミナールーム

21F に上るには 1F または B2F からエレベーターで 7F に上って、そこからさらに 21F に上がるエレベーターにのってください。

注意事項