| 2016 | Verifying Concurrent Graph Algorithms. | Azalea Raad, Aquinas Hobor, Jules Villard, Philippa Gardner |
| 2016 | Refined Environment Classifiers - Type- and Scope-Safe Code Generation with Mutable Cells. | Oleg Kiselyov, Yukiyoshi Kameyama, Yuto Sudo |
| 2016 | Probabilistic Programming Language and its Incremental Evaluation. | Oleg Kiselyov |
| 2016 | Binary Session Types for Psi-Calculi. | Hans Httel |
| 2016 | Completeness for a First-Order Abstract Separation Logic. | Zhe Hou, Alwen Tiu |
| 2016 | Implementing Cantor's Paradise. | Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto |
| 2016 | A Realizability Interpretation for Intersection and Union Types. | Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, Claude Stolze |
| 2016 | Substructural Proofs as Automata. | Henry DeYoung, Frank Pfenning |
| 2016 | Learning a Strategy for Choosing Widening Thresholds from a Large Codebase. | Sooyoung Cha, Sehun Jeong, Hakjoo Oh |
| 2016 | A Debugger-Cooperative Higher-Order Contract System in Python. | Ryoya Arai, Shigeyuki Sato, Hideya Iwasaki |
| 2016 | Open Call-by-Value. | Beniamino Accattoli, Giulio Guerrieri |
| 2016 | Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models. | Tatsuya Abe, Toshiyuki Maeda |
| 2015 | Programming with "Big Code". | Eran Yahav |
| 2015 | Uncovering JavaScript Performance Code Smells Relevant to Type Mutations. | Xiao Xiao, Shi Han, Charles Zhang, Dongmei Zhang |
| 2015 | Quasi-Linearizability is Undecidable. | Chao Wang, Yi Lv, Gaoang Liu, Peng Wu |
| 2015 | Memory-Efficient Tail Calls in the JVM with Imperative Functional Objects. | Toms Tauber, Xuan Bi, Zhiyuan Shi, Weixin Zhang, Huang Li, Zhenrui Zhang, Bruno C. d. S. Oliveira |
| 2015 | Separation Logic with Monadic Inductive Definitions and Implicit Existentials. | Makoto Tatsuta, Daisuke Kimura |
| 2015 | Analyzing Distributed Multi-platform Java and Android Applications with ShadowVM. | Haiyang Sun, Yudi Zheng, Lubomr Bulej, Stephen Kell, Walter Binder |
| 2015 | More Sound Static Handling of Java Reflection. | Yannis Smaragdakis, George Balatsouras, George Kastrinis, Martin Bravenboer |
| 2015 | Aliasing Control in an Imperative Pure Calculus. | Marco Servetto, Elena Zucca |
| 2015 | Shifting the Blame - A Blame Calculus with Delimited Control. | Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi |
| 2015 | From Call-by-Value to Interaction by Typed Closure Conversion. | Ulrich Schpp |
| 2015 | Detection of Redundant Expressions: A Complete and Polynomial-Time Algorithm in SSA. | Rekha R. Pai |
| 2015 | Fault-Tolerant Resource Reasoning. | Gian Ntzik, Pedro da Rocha Pinto, Philippa Gardner |
| 2015 | Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. | Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno |