Mercurial > hg > Members > atton > seminar_slides
changeset 93:31eb02af947e
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Jan 2015 16:57:35 +0900 |
parents | 545c3b91479e |
children | 624a76d07c20 |
files | slides/20150129/slide.md |
diffstat | 1 files changed, 32 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/20150129/slide.md Thu Jan 29 16:57:35 2015 +0900 @@ -0,0 +1,32 @@ +title: Categorical Formalization of Program Modification +author: Yasutaka Higa +profile: +lang: Japanese + + +# 研究目的 (Categorical Formalization) +* プログラムの信頼性を向上させるために開発手法に着目する +* プログラムの信頼性が変化するのはプログラムを変更した時である +* 信頼性を保ちながらプログラムを変更にプログラムの変更を形式化する + +# 研究目的 (Parallel Debugger) +* 本研究では Monad を用いてプログラムの変更を定義する +* Monad とは meta computation とデータ構造を対応付ける手法である +* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する +* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する + +# 近況報告 +* 長さ制限付きの無限長 Delta の証明ができました +* そのおかげで DeltaM の unity-law の1つはできました + * が、もう片方が無理です + +# つまってるところ +``` + (f ≡ g) -> (fmap f x ≡ fmap g x) +``` + +* ができない +* refl, cong, sym, trans でも無いので +* これができないと書けそうもない状態ですね + +<!-- vim: set filetype=markdown.slide: -->