イベントの説明
証明器Coqの解説書 Coq'Art を読む読書会だったのですが、まずは ソフトウェアの基礎 を読むことになりました。しばらくは本を購入する必要はありません。Webで公開されている資料を使って勉強を進めます。
主催者は証明器についてまったくの素人なので、基本からしっかり勉強する読書会にしようと思っています。「Coqって何？」という方は以下のリンクが参考になるかもしれません。
| 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 ソフトウェアの基礎 の担当部分を発表(Smallstep_J の smallstep_bool_shortcut から始めます) or 各自証明
- 18:30-20:00 懇親会(有志)
持ち物
- Coq をインストールしたノートPC (ハンズオンを行なうので必ず持ってきてください！) [https://github.com/sfja/sfja] を自分のノートPCにgit cloneしておいてください
- 全てが型付けされた世界を泳ぐ純粋な心
集合場所
歌舞伎座タワー 21F セミナールーム
21F に上るには 1F または B2F からエレベーターで 7F に上って、そこからさらに 21F に上がるエレベーターにのってください。
資料 資料をもっと見る／編集する
資料が投稿されると、最新の3件が表示されます。
フィード
2016/01/19 15:54
SF読み進捗ダメです会議 #25 #readcoqart #Coq を公開しました！
tmiya_
khibino
eldesh
エンジニアをつなぐ
connpass は株式会社ビープラウドが開発・運営しています