π calculus

なんが学生が話題に出してて。どこで見つけてきた? 自分が手元にもってるのは、

　　Communication and Concurrency

ですけどね。自分は Clocked な Temporal logic やってきてて、その頃は λ calculus はやってはいたけど、

　　CCS 何もの?

ってのは結構あってな。慶應の人たちとお勉強したのは懐かしい。今、見直してみると、

　　並行動作するλ項の操作的意味論
　　仕様記述の時相論理

別に普通っちゃ普通。bisimulation よりは language containment ってのは用語の違いだけか。

Temporal logic of actions ってのもあって、みんないろいろ発明するものでもあるらしい。

ただ、なんか画期的な定理が示せたでもないんだよな。やさしくないってことか。

今扱ってるのでも、Agda で途中まで書いたんだが、どうも

　　途中で、検証ループに落ちる

ところがあって放置してるんだけど、もしかすると停止性の問題かも知れない。

ω automaton は、ℕ → Set みたいな形で書いてはみたが、まだ、あんまりうまくいってないかな。

まぁ、そのうち、なんか降ってくるかも。