日々の流転

λ. SLACS 2003

に行ってきた。池上さんにも久しぶりに会えたし、興味深い話も沢山聴けて、とても楽しかった。だけど、ついていけない話も多くて結構悔しい。懇親会にも参加してきた。

λ. Modal logics for coalgebras -- A Survey, 蓮尾 一郎 (東工大)

そういえば、これまで bisimilarity と behavioral equivalence は同じだと思い込んでいて少し恥ずかしかった。本当は、bisimilarity の方が一般には強い条件で、関手Tがweak pullback を保存するならば同値になるのか。

• Technical Report

λ. Regular category の中の非決定性オートマトン, 池上 大介 (産総研/CREST)

最初は割と簡単かなと思っていたら、いつの間にか付いていけなくなっていた。気になっていた話の一つだったので悔しい。Adámek らのアプローチ(cf Automata and Algebras in Categories)の特殊な場合になってるらしい。

λ. 抽象解釈にみられる圏論的構成について, 西澤 弘毅 (東大/産総研)

抽象解釈(abstract interpretation)って名前はよく聞くけどどういうものか知らなかったので、その辺りが良くわかって嬉しかった。今回聴いた発表のなかでちゃんと理解できたのはこれだけかも。

λ. 明示的代入計算の強正規化性の証明について, 桜井貴文 (千葉大)

.

λ. 様相μ計算の完全性について, 鹿島 亮 (東工大)

様相μ計算というのは、様相命題論理の体系に不動点演算子を加えたもの……なのかな。そういう事は全然考えたことが無かったので新鮮に感じた。よくは分からなかったけど。

λ. Announcement of Typed Lambda Calculus and Applications, 長谷川真人 (京大)

国際学会 "Typed Lambda Calculus and Applications" のアナウンス。2005年奈良。typed lambda calculus というタイトルだけど、untypedでも、λ以外でも実は良いらしい。来年の10月くらいが論文の締め切りで、長さ的には15ページ程度らしい。

それから、

Fourth ACM-SIGPLAN Continuation Workshop (CW'04)

deadlineは10/1。

Category Theory in Computer Science (CTCS 2004)

コペンハーゲン。カテゴリの「カ」の字でも入ってればOKらしい (笑)

なんてのもあるそう。

それから、線形論理では「A = (A -o ⊥) -o ⊥」「!A = (A → ⊥) -o ⊥」「?A = (A -o ⊥) → ⊥」が成り立っていて、前者の二つに関しては「A = ∀X. (A -o X) -o X」「!A = ∀X. (A → X) -o X」も言えるのに、最後のだけは「?A = ∀X. (A -o X) → X」ではなく「A = ∀X. (A -o X) → X」になるのは何故か、といった話もしていた。

λ. Flow Analytic Type System for Compiler Optimizations , 松野裕(東大)

.

λ. NP完全問題を解く決定性アルゴリズムについて, 久馬栄道 (愛知学院大)

.

λ. On Sufficient Conditions And Partial Analysis for Secure Cryptographic Protocols, Masao Mori (九大)

.