Rowan Davies, "A Temporal Logic Approach To Binding-Time Analysis"

をざっと読んだ。
時相論理(temporal logic)にnextという演算子を追加して、カリーハワード同型対応によって時相λ計算(temporal lambda calculus)というものが得られる。このtemporal lambda calculusは部分計算(partial evaluation)の解析に向いているという話らしい。
まだ詳細は読んでいないのだけれどこのmodal typeというのは結構面白い応用があるんじゃないかなと思った。ちょっと色々考えてみよう。
あと、この論文よりもっと一般的なmodal typeの話は"A Modal Analysis of Staged Computation"にあるらしい。
しかし、型理論は奥が深いな。