Thanks! Interesting. I'll try to dig out the recent papers. Although I have a feeling that most of this is not that new. LLVM is just a very basic SSA, which is early 90s. Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabelle, which are very old. There've been a lot of buzz in the concurrent code verification ever since the early pi-calculus papers by R. Milner.
But the liquid type inference seems to be a genuinely new thing, and apparently I totally missed it somehow. It even seems like I unknowingly reinvented something similar, by using arbitrary Prolog code as type attributes on top of a basic Hindley-Milner.
* Fault Location via Dynamic Slicing
* Interprocedural Analysis and the Verification of Concurrent Programs
* Logics and Algorithms for Software Model Checking
* Verifying Low-Level Programs via Liquid Type Inference
Moreover:
* Agda
* LLVM