トップ «前の日記(2007-10-11) 最新次の日記(2007-10-13)» 月表示編集

日々の流転

2007-10-12 [長年日記]

λ. 名古屋 (2)

twitterでのsoutaroさんの、PROでの某発表に関する一連の発言が面白かった。

これはひどいな (11:18)
ずっとakr師匠のターン (11:18)
まじでフルボッコだな・・・ (11:30)
師匠、そろそろ自重ｗｗｗｗｗ (11:32)

OCaml-Nagoyaの飲み会に参加。

CoqとAgda
- dependent product と dependent sum
  - dependent sum: Σa:A.B(a) = B(a1) + B(a2) + …
  - dependent product: Πa:A.B(a) = B(a1) × B(a2) × …
- equality
  - Leibniz equality
  - Inductive equality
  - Extensional equality
- 停止性検査
非同期π
ネットカフェ遊牧民 (一体何を遊牧してるのだろう……)

javascriptでcall/ccを実現する話があったが、Concurrent.Threadのコードを流用すると簡単に実現できるのではないかと思う。

Coq上で普通の数学を展開するのはそんなに自明な話ではないと思う。

古典論理と直観主義論理の違い
一階述語論理と高階述語論理の違い
集合論と型理論との違い

関連

[ツッコミを入れる]