Mercurial > hg > Papers > 2015 > atton-sigse

changeset 54:40344cc2c590 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add position by kono-teacher
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 22 Jan 2015 22:24:55 +0900
parents 65391f6321a8
children
files slide/slide.html slide/slide.md
diffstat 2 files changed, 246 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/slide/slide.html	Thu Jan 22 10:49:27 2015 +0900
+++ b/slide/slide.html	Thu Jan 22 22:24:55 2015 +0900
@@ -36,7 +36,7 @@
 			<!-- === begin markdown block ===
 
       generated by markdown 1.1.1 on Ruby 2.2.0 (2014-12-25) [x86_64-darwin13]
-                on 2015-01-22 10:48:46 +0900 with Markdown engine kramdown (1.4.2)
+                on 2015-01-22 22:24:17 +0900 with Markdown engine kramdown (1.4.2)
                   using options {}
   -->
 
@@ -44,9 +44,8 @@
 
 <ul>
   <li>大学ではどんなことをやっているか(講義, イベント, 研究)</li>
-  <li>講義などでつまづくポイント</li>
-  <li>つまづきの解決策</li>
-  <li>どのような講義をするべきか?</li>
+  <li>ポジション(河野)</li>
+  <li>ポジション(比嘉)</li>
 </ul>
 
 
@@ -133,7 +132,7 @@
   <li>集合, 論理, 関数, 自然演繹による証明</li>
   <li>型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明</li>
   <li>Haskell : 自然演繹と lambda calculus</li>
-  <li>Agda    : Data type に対する証明 (Product, Sum, List, Functor, Monad …)</li>
+  <li>Agda    : Category, Data type の証明 (Product, Sum, List, Functor, Monad …)</li>
   <li>Agda    : SystemT を使った自然数に対する演算の証明</li>
 </ul>
 
@@ -164,7 +163,7 @@
 <div class="slide" id="8"><div>
 		<section>
 			<header>
-				<h1 id="section-3">圏によるプログラムの形式化</h1>
+				<h1 id="delta-monad">圏によるプログラムの形式化 : Delta Monad</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -184,7 +183,177 @@
 <div class="slide" id="9"><div>
 		<section>
 			<header>
-				<h1 id="section-4">学習コスト</h1>
+				<h1 id="section-3">ポジション(河野)</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>形式手法を学習するには</li>
+  <li>形式手法とツール</li>
+  <li>形式手法とワークフロー</li>
+  <li>形式手法と証明</li>
+  <li>形式手法の将来</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="10"><div>
+		<section>
+			<header>
+				<h1 id="section-4">形式手法を学習するには</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>学習するには本や論文を読み、問題を一つ一つ解いていく必要がある
+    <ul>
+      <li>長く手間がかかる作業</li>
+      <li>一方でルールの適用なので誰がやっても結果は同じ</li>
+      <li>難しいのはルールの適用から意味のある結果を得ること</li>
+      <li>そこが想像できないと「わからない」ということになる</li>
+      <li>わからないのではなくて、わかることに価値を見出せなくなる</li>
+    </ul>
+  </li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="11"><div>
+		<section>
+			<header>
+				<h1 id="section-5">形式手法とツール</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>実際の形式ツールを使うためには
+    <ul>
+      <li>どういうツールがあるのか調べる</li>
+      <li>環境を作ってそのツールを理解する</li>
+    </ul>
+  </li>
+  <li>使いこなすことでバグが取れたとして
+    <ul>
+      <li>その利益はどこにあるのか</li>
+      <li>研究開発が速くなるのか, 質が良くなるのか</li>
+    </ul>
+  </li>
+  <li>理解して使う必要がある</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="12"><div>
+		<section>
+			<header>
+				<h1 id="section-6">形式手法とワークフロー</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>研究開発は分散版管理を用いて行なわれている
+    <ul>
+      <li>Pull Request, Project Management Tool などで研究状況を認識</li>
+    </ul>
+  </li>
+  <li>分散版管理そのものは形式的に定義できると考えている
+    <ul>
+      <li>Delta Monad というものを提案している</li>
+    </ul>
+  </li>
+  <li>学んで理解する教育手順そのものを研究室のワークフローとしたい
+    <ul>
+      <li>ツールを組み込んだワークフローが有効であることを示したい</li>
+      <li>例) Pull Requeset 単位での model checking</li>
+    </ul>
+  </li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="13"><div>
+		<section>
+			<header>
+				<h1 id="section-7">形式手法と証明</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>Agda は積極的に導入している
+    <ul>
+      <li>時間がかかるので使いどころは限られる</li>
+    </ul>
+  </li>
+  <li>形式手法を学んだり証明の見落しを調べるのに便利</li>
+  <li>証明を研究開発の過程に組込むのは難しい
+    <ul>
+      <li>しかし方向性を示すのに用いることはできる</li>
+    </ul>
+  </li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="14"><div>
+		<section>
+			<header>
+				<h1 id="section-8">形式手法の将来</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>将来的にプログラムのかなりの部分は証明される
+    <ul>
+      <li>ライブラリもほとんど論文では証明が存在する</li>
+      <li>形式手法で示すことは信頼性のにも繋がる</li>
+      <li>しかしプログラム全体に広めるのは時間がかかるしできるか不明</li>
+    </ul>
+  </li>
+  <li>形式手法の基本を理解し、いくつかのツールを使える人材を企業に送りこむのが良い</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="15"><div>
+		<section>
+			<header>
+				<h1 id="section-9">ポジション(比嘉)</h1>
+			</header>
+			<!-- _S9SLIDE_ -->
+
+<ul>
+  <li>講義などでつまづいたポイント</li>
+  <li>つまづきの解決策</li>
+  <li>どのような講義をするべきか?</li>
+</ul>
+
+
+
+		</section>
+</div></div>
+
+<div class="slide" id="16"><div>
+		<section>
+			<header>
+				<h1 id="section-10">学習コスト</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -201,10 +370,10 @@
 		</section>
 </div></div>
 
-<div class="slide" id="10"><div>
+<div class="slide" id="17"><div>
 		<section>
 			<header>
-				<h1 id="section-5">つまづくポイント</h1>
+				<h1 id="section-11">つまづくポイント</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -224,10 +393,10 @@
 		</section>
 </div></div>
 
-<div class="slide" id="11"><div>
+<div class="slide" id="18"><div>
 		<section>
 			<header>
-				<h1 id="section-6">つまづきをどう解決するか</h1>
+				<h1 id="section-12">つまづきをどう解決するか</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -251,10 +420,10 @@
 		</section>
 </div></div>
 
-<div class="slide" id="12"><div>
+<div class="slide" id="19"><div>
 		<section>
 			<header>
-				<h1 id="section-7">他に講義に取りいれるもの?</h1>
+				<h1 id="section-13">他に講義に取りいれるもの?</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -278,7 +447,7 @@
 		</section>
 </div></div>
 
-<div class="slide" id="13"><div>
+<div class="slide" id="20"><div>
 		<section>
 			<header>
 				<h1 id="delta-">データ構造 Delta の定義</h1>
@@ -304,7 +473,7 @@
 		</section>
 </div></div>
 
-<div class="slide" id="14"><div>
+<div class="slide" id="21"><div>
 		<section>
 			<header>
 				<h1 id="delta--monad--instance-">Delta に対する Monad の instance 定義</h1>
@@ -328,10 +497,10 @@
 		</section>
 </div></div>
 
-<div class="slide" id="15"><div>
+<div class="slide" id="22"><div>
 		<section>
 			<header>
-				<h1 id="section-8">元のプログラムとプログラムの変更</h1>
+				<h1 id="section-14">元のプログラムとプログラムの変更</h1>
 			</header>
 			<!-- _S9SLIDE_ -->
 
@@ -342,7 +511,7 @@
 		</section>
 </div></div>
 
-<div class="slide" id="16"><div>
+<div class="slide" id="23"><div>
 		<section>
 			<header>
 				<h1 id="delta--1">Delta によって記述されたプログラムの実行</h1>
@@ -356,7 +525,7 @@
 		</section>
 </div></div>
 
-<div class="slide" id="17"><div>
+<div class="slide" id="24"><div>
 		<section>
 			<header>
 				<h1 id="delta--2">Delta のメリット</h1>
--- a/slide/slide.md	Thu Jan 22 10:49:27 2015 +0900
+++ b/slide/slide.md	Thu Jan 22 22:24:55 2015 +0900
@@ -5,9 +5,8 @@
 
 # Agenda
 * 大学ではどんなことをやっているか(講義, イベント, 研究)
-* 講義などでつまづくポイント
-* つまづきの解決策
-* どのような講義をするべきか?
+* ポジション(河野)
+* ポジション(比嘉)
 
 # 講義で使用している形式手法
 * 仕様記述
@@ -33,7 +32,7 @@
 * 集合, 論理, 関数, 自然演繹による証明
 * 型システム, Curry-Howard Isomorphism を通して Haskell, Agda で証明
 * Haskell : 自然演繹と lambda calculus
-* Agda    : Data type に対する証明 (Product, Sum, List, Functor, Monad ...)
+* Agda    : Category, Data type の証明 (Product, Sum, List, Functor, Monad ...)
 * Agda    : SystemT を使った自然数に対する演算の証明
 
 # Agda による証明を解説した例
@@ -42,13 +41,67 @@
 * Agda で SystemT の Nat の加法の交換法則を解説
 * 定義の解説にほとんどの時間を取られてしまう
 
-# 圏によるプログラムの形式化
+# 圏によるプログラムの形式化 : Delta Monad
 * プログラムの変更を Monad で表す
 * プログラムの変更時に変更前のプログラムも残したまま変更する
 * 全てのバージョンのプログラムを同時に実行できる
 * デバッグやテストと組み合せることでバグを見付けたい
 * 実行系と検証系を同時に走らせることもできる
 
+# ポジション(河野)
+* 形式手法を学習するには
+* 形式手法とツール
+* 形式手法とワークフロー
+* 形式手法と証明
+* 形式手法の将来
+
+# 形式手法を学習するには
+* 学習するには本や論文を読み、問題を一つ一つ解いていく必要がある
+    * 長く手間がかかる作業
+    * 一方でルールの適用なので誰がやっても結果は同じ
+    * 難しいのはルールの適用から意味のある結果を得ること
+    * そこが想像できないと「わからない」ということになる
+    * わからないのではなくて、わかることに価値を見出せなくなる
+
+# 形式手法とツール
+* 実際の形式ツールを使うためには
+    * どういうツールがあるのか調べる
+    * 環境を作ってそのツールを理解する
+* 使いこなすことでバグが取れたとして
+    * その利益はどこにあるのか
+    * 研究開発が速くなるのか, 質が良くなるのか
+* 理解して使う必要がある
+
+# 形式手法とワークフロー
+* 研究開発は分散版管理を用いて行なわれている
+    * Pull Request, Project Management Tool などで研究状況を認識
+* 分散版管理そのものは形式的に定義できると考えている
+    * Delta Monad というものを提案している
+* 学んで理解する教育手順そのものを研究室のワークフローとしたい
+    * ツールを組み込んだワークフローが有効であることを示したい
+    * 例) Pull Requeset 単位での model checking
+
+# 形式手法と証明
+* Agda は積極的に導入している
+    * 時間がかかるので使いどころは限られる
+* 形式手法を学んだり証明の見落しを調べるのに便利
+* 証明を研究開発の過程に組込むのは難しい
+    * しかし方向性を示すのに用いることはできる
+
+# 形式手法の将来
+* 将来的にプログラムのかなりの部分は証明される
+    * ライブラリもほとんど論文では証明が存在する
+    * 形式手法で示すことは信頼性のにも繋がる
+    * しかしプログラム全体に広めるのは時間がかかるしできるか不明
+* 形式手法の基本を理解し、いくつかのツールを使える人材を企業に送りこむのが良い
+
+
+
+# ポジション(比嘉)
+* 講義などでつまづいたポイント
+* つまづきの解決策
+* どのような講義をするべきか?
+
 # 学習コスト
 * 論理, 自然演繹 -> Haskell -> Agda
 * それぞれのステップに壁がある