# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1479812347 -32400
# Node ID 4f668900d1f68fa330d8db763c231b7c4612b0c2
# Parent  1fb4897cc67fa67525d250b27a07a953d82415ba
Add slide

diff -r 1fb4897cc67f -r 4f668900d1f6 slides/20161122/slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20161122/slide.md	Tue Nov 22 19:59:07 2016 +0900
@@ -0,0 +1,32 @@
+title: Verification method of programs using Continuation based C
+author: Yasutaka Higa
+profile:
+lang: Japanese
+
+# 研究目的
+* コードセグメントとデータセグメントという単位を用いてプログラムを記述する手法を提案する
+* プログラムはコードセグメントという処理の集合として表され、相互に接続される
+* 型検査器を導入することでコードセグメントが接続可能かどうかを判断する
+* また、コードセグメントの型から推論してデータセグメントの生成を行なう
+
+# 研究内容
+* コードセグメントとデータセグメントを用いて記述する言語 Continuation based C に型を導入する
+* コードセグメント内部の演算と変数代入から型を推論する
+* 接続可能かどうかをコンパイル時に判断し、必要なデータセグメントを型情報から生成する
+
+# 研究内容(最近)
+* Code Gear でプログラムを記述する理由に信頼性がある
+* アルゴリズムそのものを証明してやることで信頼性を確保する
+* Agda という証明支援系の言語に cbc を変換してやる
+
+# 近況報告
+* SingleLinkedStack の証明
+    * 任意の数の要素を入れて同じだけ出すと
+    * Stack は空になる
+    * 順番は逆になってる
+* 有限長の任意の要素が入る list を考える
+    * (pop * n) (push * n) list == reverse list
+    * push は a で pop は maybe a なのでlistが再構成できない
+
+
+<!-- vim: set filetype=markdown.slide: -->