Mercurial > hg > Papers > 2018 > nozomi-master

changeset 122:c195713cf7d7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update slide
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 14 Feb 2017 15:45:03 +0900
parents 137aae675a94
children 81978a9122f0
files presentation/slide.html presentation/slide.md presentation/slide.pdf.html
diffstat 3 files changed, 244 insertions(+), 70 deletions(-) [+]
line wrap: on
line diff
--- a/presentation/slide.html	Tue Feb 14 15:03:04 2017 +0900
+++ b/presentation/slide.html	Tue Feb 14 15:45:03 2017 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 15:44:26 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -129,22 +129,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">本発表ではモデル検査的アプローチについて中心に見ていきます</h1>
-<ul>
-  <li>修士論文の内部の比率は半分半分くらい</li>
-  <li>定理証明の方は説明する内容が多くて複雑</li>
-  <li>モデル検査的アプローチは過去論文を提出したもの
-    <ul>
-      <li>なのでそちらをメインで発表します</li>
-    </ul>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-3">モデル検査的アプローチについての流れ</h1>
+<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
 <ul>
   <li>既存のモデル検査器について</li>
   <li>Continuation based C (CbC) 言語について</li>
@@ -266,7 +251,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">メタ計算</h1>
+<h1 id="section-3">メタ計算</h1>
 <ul>
   <li>とある計算を実現するための計算</li>
   <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
@@ -320,7 +305,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-5">赤黒木</h1>
+<h1 id="section-4">赤黒木</h1>
 <ul>
   <li>データの保存に用いる二分木</li>
   <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
@@ -353,7 +338,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-6">仕様の記述とその確認</h1>
+<h1 id="section-5">仕様の記述とその確認</h1>
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
@@ -371,14 +356,14 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-7">チェックする仕様</h1>
+<h1 id="section-6">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
     <ul>
       <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
     </ul>
   </li>
-  <li>以下のような条件式を仕様として CbC で定義、検証できる</li>
+  <li>以下のような条件式を仕様として CbC で定義できる</li>
 </ul>
 
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
@@ -405,7 +390,7 @@
           <li>赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……</li>
         </ul>
       </li>
-      <li>その度に仕様の式は成り立つかをチェックする</li>
+      <li>挿入する度に仕様の式が成り立つかをチェック</li>
     </ul>
   </li>
   <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
@@ -456,6 +441,57 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda-">Agda における証明</h1>
+<ul>
+  <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
+    <ul>
+      <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
+    </ul>
+  </li>
+  <li>論理式は型に相当して、証明はその値の導出</li>
+  <li>三段論法の証明は以下のようになる
+    <ul>
+      <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>f : {A B C : Set} -&gt; ((A -&gt; B) × (B -&gt; C)) -&gt; (A -&gt; C)
+f = \p x -&gt; (snd p) ((fst p) x)
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda--1">Agda における等式の証明</h1>
+<ul>
+  <li>Agda では等式も証明できる
+    <ul>
+      <li>依存型という型を変数として扱える型システムを持つ</li>
+      <li>型を取って型を返す型などが定義可能</li>
+    </ul>
+  </li>
+  <li>等式の証明は両方が同じ項に簡約されることを示せば良い</li>
+  <li>自然数の加法の交換法則は以下のようになる</li>
+</ul>
+
+<pre><code>addSym : (n m : Nat) -&gt; n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
+  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
   <li>CbC の DataSegment は Agda のレコード型
@@ -503,7 +539,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-8">メタレベルの型付け</h1>
+<h1 id="section-7">メタレベルの型付け</h1>
 <ul>
   <li>メタ計算とは通常のレベルとは区別された計算</li>
   <li>任意の通常のレベルの計算を扱えなくてはならない
@@ -524,7 +560,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="agda-">Agda 上のメタ計算</h1>
+<h1 id="agda--2">Agda 上のメタ計算</h1>
 <ul>
   <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる
     <ul>
@@ -549,6 +585,34 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda--3">Agda 上で証明できた性質</h1>
+<ul>
+  <li>CodeSegment の合成則</li>
+</ul>
+
+<pre><code>comp-associative : &gt; (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -&gt; csComp  c (csComp b a) ≡ csComp  (csComp c b) a
+comp-associative (cs _) (cs _) (cs _) = refl
+-- c . (b . a) ≡ (c . b) . a
+</code></pre>
+
+<ul>
+  <li>スタックの操作についての性質</li>
+</ul>
+
+<pre><code>push-pop-type : ℕ -&gt; ℕ  -&gt; ℕ -&gt; Element ℕ -&gt; Set₁
+push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+-- goto (pop . push) mds ≡ mds
+
+n-push-pop-type : ℕ -&gt;  ℕ  -&gt; ℕ -&gt; SingleLinkedStack ℕ -&gt; Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
+-- goto (pop*n . push*n) mds ≡ mds
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--cbc-">Agda 上に CbC を記述した成果</h1>
 <ul>
   <li>部分型で CbC の型付けができた</li>
@@ -568,13 +632,13 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-9">まとめ</h1>
+<h1 id="section-8">まとめ</h1>
 <ul>
   <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li>
   <li>モデル検査的なアプローチ
     <ul>
       <li>継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装</li>
-      <li>有限の要素数まで保証できた</li>
+      <li>有限の要素数まで検証できた</li>
     </ul>
   </li>
   <li>証明的なアプローチ
@@ -590,20 +654,19 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-10">今後の課題</h1>
+<h1 id="section-9">今後の課題</h1>
 <ul>
   <li>より大きなサイズの赤黒木の検証</li>
   <li>赤黒木の挿入に関する性質を証明する</li>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
-  <li>型情報から stub を自動生成すkる</li>
 </ul>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-11">発表履歴</h1>
+<h1 id="section-10">発表履歴</h1>
 <ul>
   <li>Agda 入門.
     <ul>
--- a/presentation/slide.md	Tue Feb 14 15:03:04 2017 +0900
+++ b/presentation/slide.md	Tue Feb 14 15:45:03 2017 +0900
@@ -21,12 +21,6 @@
     * 型システムを通して CbC の形式的な定義を得る
     * SingleLinkedStack の性質の証明
 
-# 本発表ではモデル検査的アプローチについて中心に見ていきます
-* 修士論文の内部の比率は半分半分くらい
-* 定理証明の方は説明する内容が多くて複雑
-* モデル検査的アプローチは過去論文を提出したもの
-    *  なのでそちらをメインで発表します
-
 # モデル検査的アプローチについての流れ
 * 既存のモデル検査器について
 * Continuation based C (CbC) 言語について
@@ -153,7 +147,7 @@
 # チェックする仕様
 * 赤黒木の高さに関する仕様に以下のものがある
     * 木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる
-* 以下のような条件式を仕様として CbC で定義、検証できる
+* 以下のような条件式を仕様として CbC で定義できる
 
 ```
 __code verifySpecificationFinish(struct Context* context) {
@@ -171,7 +165,7 @@
 * メタ計算としてプログラムの状態を数え上げる
     * goto された時に挿入される要素の組み合わせを全て列挙して実行する
         * 赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……
-    * その度に仕様の式は成り立つかをチェックする
+    * 挿入する度に仕様の式が成り立つかをチェック
 * ノーマルレベルのコードを検証用に変更せず検証可能
 
 ![akashaPut](./images/akashaPut.svg){:width="50%"}
@@ -194,6 +188,38 @@
     * しかし CbC の形式的な定義が無いために今はできない
 * Agda 上に CbC を定義することで形式的な定義を得る
 
+# Agda における証明
+* Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
+    * 自然演繹: 命題、ならば、かつ、または、で構成される証明システム
+* 論理式は型に相当して、証明はその値の導出
+* 三段論法の証明は以下のようになる
+    * 「((A ならば B) かつ (B ならば C)) ならば (A ならば C)
+
+```
+f : {A B C : Set} -> ((A -> B) × (B -> C)) -> (A -> C)
+f = \p x -> (snd p) ((fst p) x)
+```
+
+# Agda における等式の証明
+* Agda では等式も証明できる
+    * 依存型という型を変数として扱える型システムを持つ
+    * 型を取って型を返す型などが定義可能
+* 等式の証明は両方が同じ項に簡約されることを示せば良い
+* 自然数の加法の交換法則は以下のようになる
+
+```
+addSym : (n m : Nat) -> n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
+  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎
+```
+
 # Agda と DataSegment
 * CbC の DataSegment は Agda のレコード型
     * 名前付きの値が複数ある(C の構造体)
@@ -255,6 +281,29 @@
                                  ; c' = 0 ; next = (N.cs id)})
 ```
 
+# Agda 上で証明できた性質
+* CodeSegment の合成則
+
+```
+comp-associative : > (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -> csComp  c (csComp b a) ≡ csComp  (csComp c b) a
+comp-associative (cs _) (cs _) (cs _) = refl
+-- c . (b . a) ≡ (c . b) . a
+```
+
+* スタックの操作についての性質
+
+```
+push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
+push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+-- goto (pop . push) mds ≡ mds
+
+n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
+-- goto (pop*n . push*n) mds ≡ mds
+```
+
+
 # Agda 上に CbC を記述した成果
 * 部分型で CbC の型付けができた
 * メタ計算をきちんと階層化できた
@@ -266,7 +315,7 @@
 * Continuation based C 言語を対象にした二種類の検証アプローチ
 * モデル検査的なアプローチ
     * 継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装
-    * 有限の要素数まで保証できた
+    * 有限の要素数まで検証できた
 * 証明的なアプローチ
     * 証明支援系 Agda 上で CbC のプログラムを定義して直接証明
     * 部分型を利用して CbC を型付け
@@ -277,7 +326,6 @@
 * 赤黒木の挿入に関する性質を証明する
 * 部分型を利用してCbCを型付け
 * 依存型をCbC に導入して自身を証明可能にする
-* 型情報から stub を自動生成すkる
 
 # 発表履歴
 * Agda 入門.
--- a/presentation/slide.pdf.html	Tue Feb 14 15:03:04 2017 +0900
+++ b/presentation/slide.pdf.html	Tue Feb 14 15:45:03 2017 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 15:02:42 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 15:44:26 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -113,22 +113,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">本発表ではモデル検査的アプローチについて中心に見ていきます</h1>
-<ul>
-  <li>修士論文の内部の比率は半分半分くらい</li>
-  <li>定理証明の方は説明する内容が多くて複雑</li>
-  <li>モデル検査的アプローチは過去論文を提出したもの
-    <ul>
-      <li>なのでそちらをメインで発表します</li>
-    </ul>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h1 id="section-3">モデル検査的アプローチについての流れ</h1>
+<h1 id="section-2">モデル検査的アプローチについての流れ</h1>
 <ul>
   <li>既存のモデル検査器について</li>
   <li>Continuation based C (CbC) 言語について</li>
@@ -250,7 +235,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">メタ計算</h1>
+<h1 id="section-3">メタ計算</h1>
 <ul>
   <li>とある計算を実現するための計算</li>
   <li>ネットワーク接続、例外処理、メモリ確保、並列処理など</li>
@@ -304,7 +289,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-5">赤黒木</h1>
+<h1 id="section-4">赤黒木</h1>
 <ul>
   <li>データの保存に用いる二分木</li>
   <li>特に赤黒木はノードが持つ赤か黒の色を使って木のバランスを取る
@@ -337,7 +322,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-6">仕様の記述とその確認</h1>
+<h1 id="section-5">仕様の記述とその確認</h1>
 <ul>
   <li>「バランスが取れている」とは何かを表現できる必要がある
     <ul>
@@ -355,14 +340,14 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-7">チェックする仕様</h1>
+<h1 id="section-6">チェックする仕様</h1>
 <ul>
   <li>赤黒木の高さに関する仕様に以下のものがある
     <ul>
       <li>木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる</li>
     </ul>
   </li>
-  <li>以下のような条件式を仕様として CbC で定義、検証できる</li>
+  <li>以下のような条件式を仕様として CbC で定義できる</li>
 </ul>
 
 <pre><code>__code verifySpecificationFinish(struct Context* context) {
@@ -389,7 +374,7 @@
           <li>赤黒木の状態の保存、挿入、チェック、次の状態の列挙、赤黒木の再現……</li>
         </ul>
       </li>
-      <li>その度に仕様の式は成り立つかをチェックする</li>
+      <li>挿入する度に仕様の式が成り立つかをチェック</li>
     </ul>
   </li>
   <li>ノーマルレベルのコードを検証用に変更せず検証可能</li>
@@ -440,6 +425,57 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda-">Agda における証明</h1>
+<ul>
+  <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
+    <ul>
+      <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
+    </ul>
+  </li>
+  <li>論理式は型に相当して、証明はその値の導出</li>
+  <li>三段論法の証明は以下のようになる
+    <ul>
+      <li>「((A ならば B) かつ (B ならば C)) ならば (A ならば C)</li>
+    </ul>
+  </li>
+</ul>
+
+<pre><code>f : {A B C : Set} -&gt; ((A -&gt; B) × (B -&gt; C)) -&gt; (A -&gt; C)
+f = \p x -&gt; (snd p) ((fst p) x)
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="agda--1">Agda における等式の証明</h1>
+<ul>
+  <li>Agda では等式も証明できる
+    <ul>
+      <li>依存型という型を変数として扱える型システムを持つ</li>
+      <li>型を取って型を返す型などが定義可能</li>
+    </ul>
+  </li>
+  <li>等式の証明は両方が同じ項に簡約されることを示せば良い</li>
+  <li>自然数の加法の交換法則は以下のようになる</li>
+</ul>
+
+<pre><code>addSym : (n m : Nat) -&gt; n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
+  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--datasegment">Agda と DataSegment</h1>
 <ul>
   <li>CbC の DataSegment は Agda のレコード型
@@ -487,7 +523,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-8">メタレベルの型付け</h1>
+<h1 id="section-7">メタレベルの型付け</h1>
 <ul>
   <li>メタ計算とは通常のレベルとは区別された計算</li>
   <li>任意の通常のレベルの計算を扱えなくてはならない
@@ -508,7 +544,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="agda-">Agda 上のメタ計算</h1>
+<h1 id="agda--2">Agda 上のメタ計算</h1>
 <ul>
   <li>ノーマルレベルの型を保持したままメタレベルの計算を利用できる
     <ul>
@@ -533,6 +569,34 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
+<h1 id="agda--3">Agda 上で証明できた性質</h1>
+<ul>
+  <li>CodeSegment の合成則</li>
+</ul>
+
+<pre><code>comp-associative : &gt; (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -&gt; csComp  c (csComp b a) ≡ csComp  (csComp c b) a
+comp-associative (cs _) (cs _) (cs _) = refl
+-- c . (b . a) ≡ (c . b) . a
+</code></pre>
+
+<ul>
+  <li>スタックの操作についての性質</li>
+</ul>
+
+<pre><code>push-pop-type : ℕ -&gt; ℕ  -&gt; ℕ -&gt; Element ℕ -&gt; Set₁
+push-pop-type n e x s = M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+-- goto (pop . push) mds ≡ mds
+
+n-push-pop-type : ℕ -&gt;  ℕ  -&gt; ℕ -&gt; SingleLinkedStack ℕ -&gt; Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop  n) (n-push n)) meta ≡ meta
+-- goto (pop*n . push*n) mds ≡ mds
+</code></pre>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
 <h1 id="agda--cbc-">Agda 上に CbC を記述した成果</h1>
 <ul>
   <li>部分型で CbC の型付けができた</li>
@@ -552,13 +616,13 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-9">まとめ</h1>
+<h1 id="section-8">まとめ</h1>
 <ul>
   <li>Continuation based C 言語を対象にした二種類の検証アプローチ</li>
   <li>モデル検査的なアプローチ
     <ul>
       <li>継続を上書きして可能な状態を数え上げるメタ計算ライブラリ akasha を実装</li>
-      <li>有限の要素数まで保証できた</li>
+      <li>有限の要素数まで検証できた</li>
     </ul>
   </li>
   <li>証明的なアプローチ
@@ -574,20 +638,19 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-10">今後の課題</h1>
+<h1 id="section-9">今後の課題</h1>
 <ul>
   <li>より大きなサイズの赤黒木の検証</li>
   <li>赤黒木の挿入に関する性質を証明する</li>
   <li>部分型を利用してCbCを型付け</li>
   <li>依存型をCbC に導入して自身を証明可能にする</li>
-  <li>型情報から stub を自動生成すkる</li>
 </ul>
 
 
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-11">発表履歴</h1>
+<h1 id="section-10">発表履歴</h1>
 <ul>
   <li>Agda 入門.
     <ul>