日々の流転

λ. Workshop on Linear Logic, Proof Theory and Computer Science (with Lecture Series by Jean-Yves Girard)

に行ってきた。 syd_sydさんやいろんな人にお会いできた。

疲れた。

Jean-Yves Girard (Marseille, IML), “Evolutions of Proof Theory Part I”

生の Jean-Yves Girald にワクワクドキドキ。

• internal と external がなんか良くわからなかった。
• Quantum coherent space とか Hilbert space とか色々わけわからん

昼食

初(UBU)

Naoki Kobayashi (Tohoku University), “Linearity and Order in Type Systems for Programming Languages”

わかりやすい。

f: File(R)

read once

f: File(C)

close once

f: !File(R)

read arbitary times

f: !File(R); File(C)

任意の回数読まれた後に閉じられる

XMLの処理の話を以前にちょっと聞いたときには、Lazyな関数型言語でパースも木の変換も全部lazyにやればいいじゃんと思ったものだが、あるマナーに沿ってトラバースしていることを保障する型システムは非常に面白いと感じた。

• Ordered linear channel types
• Orderdd linear resouce types
• Ordered lineer tree types

Martin Berger (Queen Mary, Univ of London), “Process Calculi and Interaction Types”

Aliasing があると、古典的なホーア論理の syntactic substitution に基づいた規則はうまくいかない。事前条件を詳細化する。例えば「 {(x≠y ∧ !x=7) ∨ (x=y ∧ !y=6)} y := !y + 1 {!x = 7}」。

Sylvain Salvati (NII), “Type systems for syntax”

Montague の話とか出てきてちょっと嬉しかった(ぉぃ