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: -->