充電期

不讀完 L1 doc cache 裡面的 papers 大概不會有創造力了，看能不能一週內完成。〈pi-Calculus in (Co)Inductive Type Theory〉裡面說 "[w]e can honestly say that we have a real, user-friendly interactive system for proving bisimilarity of processes"，等用了 Coq 就知道他們有沒有吹牛了 XD。另一方面，paper 裡面只做到 strong (late) bisimilarity，而我們最後需要的是 weak bisimilarity 和 process equality，所以說不定後兩者是我們要自己動手做的。

--
不過今天剩下時間我打算留給 graphical games XD。