--- a/template/slide.md	Tue Jan 17 17:18:01 2017 +0900
+++ b/template/slide.md	Tue Jan 17 17:18:41 2017 +0900
@@ -1,19 +1,21 @@
-title: Verification method of programs using Continuation based C
+title: メタ計算を用いた Continuation based C の検証手法
 author: Yasutaka Higa
 profile:
 lang: Japanese
 
 
 # 研究目的
-* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
-* プログラムはコードセグメントという処理の集合として表され、相互に接続される
-* 個々のコードセグメントを検証し、検証されたコードセグメントどうしの組み合わせによりプログラム全体を検証する
+* 動作するプログラムの信頼性を保証したい
+* そのためにコードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
+* 処理の単位であるコードセグメントはメタ計算によって相互に接続される
+* メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証する
 
 # 研究内容
-* コードセグメントとデータセグメントを用いたプログラムに対し、検証を行なう
-* コードセグメントどうしの接続の間にメタ計算として検証機構を導入する
 * コードを検証用に変更することなく、仕様を満たすか検証する
-* 検証の対象として Gears OS のデータ構造を用いる
+* 検証にはコードの状態を数え上げるモデル検査と証明の両方を用いる
+* モデル検査はコードセグメントの接続部分を変更することで実現する
+* 証明は Continuation based C 上のコードセグメントを Agda 上で記述した上で証明する
+* Agda 上でコードセグメントを記述するために CbC の型を部分型として定義する
 
 # hoge
 * fuga