A proof theory for model checking http://www.lix.polytechnique.fr/~dale/papers/linearity2016.pdf 面白そうなのだけれど、switchability と synthetic inference rules のあたりの嬉しさが良く分からず……