摘要

明天預定要講的 Calculus of Communication Systems 好像其實只有一句話耶 ─ 和 pi-Calculus 差不多 XD。語法和 pi-Calculus 只差一兩個 operators，沒有 structural congruence 而直接用 LTS 定義語意，然後同樣進入 strong bisimulation、改成 weak bisimulation 再補成 congruence 當作 process equality，複雜度沒下降多少。倒是上次被 XOO 提醒，找到 paper〈pi-Calculus in (Co)Inductive Type Theory〉做 Coq formalisation of pi-Calculus，裡面很明確地說 structural congruence + reduction 不適合做 formalisation，所以他們採用 LTS semantics 再導出 structural congruence 的那些規則。

--
看起來要做就單純是做苦工吧 XD。