# HG changeset patch # User Yasutaka Higa # Date 1422518255 -32400 # Node ID 31eb02af947ea86221b0138a185a55f0536b891b # Parent 545c3b91479e930acf758951ec8ce11811b3f66f Add slide for seminar diff -r 545c3b91479e -r 31eb02af947e slides/20150129/slide.md --- /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 でも無いので +* これができないと書けそうもない状態ですね + +