I’ve run across some recent papers relating type systems and software model-checking, and I find this subject quite fascinating – even more when I think that my student, Thorsten, has just submitted his thesis on a somehow related topic (he’s relating a type system to a verification condition generator), without even knowing about the existence of all this related work.
- M. Naik and J. Palsberg. A type system equivalent to a model checker. ACM Trans. Program. Lang. Syst., 30(5), 2008.
- N. Kobayashi and C.-H.L. Ong. A type system equivalent to modal μ-calculus model checking of recursion schemes. In LICS, 2009.
- Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko. Refinement type inference via abstract interpretation. Arxiv.org, April 2010.
I will read more! I will read more! I will read more! 
