AIM8 （二日目：午後）

• "Using a logical theory of constructions for program verification" (Andreas Sicard)：コロンビアの大学の先生。講演のスライドはこちら、アブストラクトはこちら。 logical theory of constructions (LTC)上でgeneral recursive programs（停止しないプログラム）についての推論や検証をしよう、という話か。ちょっと「本当にできるのか」みたいな雰囲気が漂ってました。