PLT界在近幾年中對哪些問題的研究有重大進展？

希望大家能積極邀請相關人士來科普

當然是這個啦，說它是20年來最大進展都不為過：

-----12.13日更新-----

首先「PLT」這個概念沒有嚴格定義，然後」重大進展「的評價標準也不好說。。。 既然有」T「（theory），我先講理論一點的，並且縮小範圍，說一個和證明論相關的話題。。

做程序驗證的應該對Separation Logic（下面稱SL）不陌生，也已經有很多基於SL的工具。
由於SL的不可判定性，目前各類自動化工具主要用SL的子集，沒有separation implication(也就是--*這個符號）；對inductive predicate的支持也十分有限。。（省略1000字）。 其實本質上看，SL不過是Boolean BI（BBI）在程序語義上的解釋，而BBI是Bunched Logic家族的一種。Bunched Implication Logic由Peter Ohearn、D.Pym提出在98年（？）提出，之後才有LICS 02的SL。

背景介紹完了，進入主題：BBI的Proof System研究。 James Brotherson、Larchey-Wendling分別在LICS 10證明了BI系列各種邏輯的undecidablity，Brotherson利用Display Calculi給出了一個proof system，由於Display規則的nondeterminition， 它不利於自動化proof search，也就不方便用機器實現。POPL 13的一文中，Jonghyun Park等人使用了Nested sequent calculi，並實現了第一個automatic theorm prover。 緊接著的TABLEAUX 13，Hou Zhe用Labelled Sequent Calculi做了一個更高效的prover。

BBI的proof theory發展了，再改點東西就可作為SL的proof system。。果不其然，次年Park、Hou又把成果發在了POPL 14上。不過要推廣實際產品中，用於優化、改良基於SL的工具（比如Facebook Infer），還有一段距離。

綜上，我認為這是一個比較大的進展。 很長時間PL圈子似乎對BBI缺少足夠重視，誰讓SL那麼有名呢，即便它有很多限制。另外做Proof Theory的似乎也不夠重視，至少BI沒有像Linear Logic那樣大紅大紫，當然全世界做Proof Theory的人也沒有幾個

說得有點亂。。如果有興趣，歡迎與我討論。。

--------補充----------
說一些和PL聯繫密切點的。。。

Type System相關的：
Dependent Type語言，Agda, Idris等等。。
Refinement Type煥發新春，感覺是從Dependent Type和Contract各取一部分，不知為什麼還挺討巧。
Gradual/Soft Typing，這點不用多說，已經影響到工業界了（TypeScript, Python 3.5...）