Mercurial > hg > Members > atton > seminar_slides
changeset 41:15aba4b4c11f
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 29 Apr 2014 17:42:46 +0900 |
parents | 1419489ba107 |
children | a10d98fd143f |
files | slides/20140429/slide.md |
diffstat | 1 files changed, 41 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/20140429/slide.md Tue Apr 29 17:42:46 2014 +0900 @@ -0,0 +1,41 @@ +title: プログラムのデバッグ支援(仮) +author: Yasutaka Higa +cover: +lang: Japanese + + +# 研究目的(仮) + +* プログラムのデバッグは複雑になることがある +* 例えば、あるif文の条件を満たすには、必要な状態がある +* そういった状態を自動で導出したい +* 証明とかすれば良い? + +# 近況報告 + +* Proofs and Types + * Curry Howard Isomorphism of System F + * cut elimination +* Integer on Agda + * add とか書いてみてます + * R を使うと割と上手くいってません + + +# Integer on Agda + +* Int から Int を作成する場合、使い方によっては作成した Int の型が確定されてしまう +* 一旦lambdaで受けるという手 + * kono先生の source はそんな感じ +* R を使うと lambda で受けるとかでなく確定されちゃう? + * R を2回使って add を定義してみたは良いものの…… + * 黄色い + * R に product が入ってるのは関係ありそう? + +# Product on Agda +* R に Product が使われてるのは関係あったりしない? +* < π1 < u , v > , π2 < u , v > > ≡ < u , v > +* が通らないのは書かれてるのではともかく +* < u , v > ≡ < u , v > +* すら黄色い…… + +<!-- vim: set filetype=markdown.slide: -->