日々の流転

λ. “A formulae-as-types interpretation of Subtractive Logic” by Tristan Crolard

昔読みかけて放置してた論文なのだけど、こないだのコルーチンの話で思い出して、読んでみた。色々と面白い。

複数の結論を持つシーケントを考えるので、判定(judgement)の書き方が、型理論の通常のそれと異なっているのが新鮮。例えばこんな感じ。

t  :  Γ ├ Δ; A
----------------------------------------------
make-coroutine t β  :  Γ ├ Δ, B^β; A - B