--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/slide.md	Wed Jan 21 16:59:03 2015 +0900
@@ -0,0 +1,78 @@
+title: 形式手法を広めるには
+author:  河野真治 <br> 比嘉健太
+profile: 琉球大学工学部情報工学科
+lang: Japanese
+
+# Agenda
+* 大学ではどんなことをやっているか(講義, イベント, 研究)
+* 講義などを通して思う教育カリキュラムに必要なもの
+* 改善案
+
+# 講義で紹介する形式手法
+* UML (いれる?)
+* model checking 的なアプローチ
+* 証明的なアプローチ
+
+# UML (いれる?)
+* モデリングと設計
+* iOS Application を作成する
+* UML で class をモデリングする
+
+# model checking 的なアプローチ
+* Operationg System の講義
+* Process/Thread Scheduling を考えた時に
+* Dead Lock を起こすような Scheduling を実際に書いて実行させる
+* Java Path Finder で Thread の実行順序を網羅的に実行する
+
+# 証明的なアプローチ
+* ソフトウェア工学 の講義
+* 集合, 論理, 関数, 自然演繹による証明
+* 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明
+* Haskell : 自然演繹と lambda calculus
+* Agda    : Data type に対する証明 (Product, Sum, List, Functor, Monad ...)
+* Agda    : SystemT を使った自然数に対する演算の証明
+
+# Agda による証明を解説した例
+* Open Source Conference
+* ソフトウェア工学で学んだ Agda の使い方を発表
+* Agda で SystemT の Nat の加法の交換法則を解説
+* ほとんどが定義の解説に時間を取られてしまう
+
+# 圏によるプログラムの形式化
+* プログラムの変更を Monad で表す
+* プログラムの変更時に変更前のプログラムも残したまま変更する
+* 全てのバージョンのプログラムを同時に実行できる
+* デバッグやテストと組み合せることでバグ
+* 実行系と検証系を同時に走らせることもできる
+
+# 学習コスト
+* 論理, 自然演繹 -> Haskell -> Agda
+* それぞれのステップに壁がある
+* 自然演繹では解けるけれど lambda term で書き直す
+* Haskell では定義できるけれど Agda で証明できない
+
+# つまづくポイント
+* Haskell -> Agda の壁を考える
+* コードを書いてる人なら型を合わせることは分かる
+* 型によって証明を書くことに繋げるには?
+    * プログラムと論理の対応を把握してもらう必要がある
+    * どうしたら把握してもらえるか?
+
+# つまづきをどう解決するか
+* 書き続ける
+* 論理とプログラムの対応を見えるようにする
+    * Agda は対話的に項を書き換えることができる
+    * どこでつまづいても情報が手に入るようにしたい
+    * 対話的に情報を引き出す手段を知る
+
+<style>
+.slide.cover H2 {
+    font-size:72px;
+}
+.slide.cover H3#author {
+    margin-top:72px;
+    font-size:42px;
+}
+</style>
+
+<!-- vim: set filetype=markdown.slide: -->