I'm not sure anything interesting happened in the PL world since 2004 besides PEGs. Please feel free to correct me if I'm wrong, I always prefer to be among the first to jump on a new bandwagon in the language design trends.
Gradual and optional typing have become a pretty big idea over the last 6-7 years, as language designers have tried to retrofit type systems onto languages that weren't designed with them.
This idea has been showing up in industry (whether the designers call it "gradual typing" or not) with at least Hack, Flow, TypeScript, and Dart (which has optional type annotations).
You can find lots of references for useful underlying theory and research applications (the first paper that mentions "gradual typing" was Siek and Taha in 2006) at https://github.com/samth/gradual-typing-bib.
Typed Racket (http://docs.racket-lang.org/ts-guide/) is probably the best-engineered exemplar of many of these ideas, especially 1. installing run-time checks at boundaries between typed and untyped code, and 2. tackling problems of typing previously untyped code that uses rich class and interface patterns.
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.
What are good examples of things in the bucket of type inference algorithms that are simpler than MLF? You must be looking for ones which infer sophisticated logics, still, otherwise that bucket will always be dominated by HM, no?
Boxy types, HMF, and bidirectional (older but more recently applied to parametric polymorphism) all leverage partial annotations to handle a more flexible parametric polymorphism than HM itself allows.
Another brilliant recent discovery (2001, so still more than a decade ago I am afraid) is the algebraic connection between differentiation and zippers. See Conor McBride's paper "The Derivative of a Regular Type is its Type of One-Hole Contex"
Even in the parser corner, the parser combinator / graph-structured stack / GLL algorithm is both new and exciting. GLL was published in 2010: http://dotat.at/tmp/gll.pdf
