| 2009 | Weak updates and separation logic. | Gang Tan, Zhong Shao, Xinyu Feng, Hongxu Cai |
| 2009 | Fractional Ownerships for Safe Memory Deallocation. | Kohei Suenaga, Naoki Kobayashi |
| 2009 | The Sketching Approach to Program Synthesis. | Armando Solar-Lezama |
| 2009 | Abstract Transformers for Thread Correlation Analysis. | Michal Segalov, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Mooly Sagiv |
| 2009 | The Higher-Order, Call-by-Value Applied Pi-Calculus. | Nobuyuki Sato, Eijiro Sumii |
| 2009 | A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming. | Shigeyuki Sato, Hideya Iwasaki |
| 2009 | Parallel Reduction in Resource Lambda-Calculus. | Michele Pagani, Paolo Tranquilli |
| 2009 | Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation. | Hakjoo Oh |
| 2009 | Scalable Context-Sensitive Points-to Analysis Using Multi-dimensional Bloom Filters. | Rupesh Nasre, Kaushik Rajan, Ramaswamy Govindarajan, Uday P. Khedker |
| 2009 | A Short Cut to Optimal Sequences. | Akimasa Morihata |
| 2009 | Ownership Downgrading for Ownership Types. | Yi Lu, John Potter, Jingling Xue |
| 2009 | Witnessing Purity, Constancy and Mutability. | Ben Lippmeier |
| 2009 | Refining Abstract Interpretation-Based Static Analyses with Hints. | Vincent Laviron, Francesco Logozzo |
| 2009 | Types and Recursion Schemes for Higher-Order Program Verification. | Naoki Kobayashi |
| 2009 | Classical Natural Deduction for S4 Modal Logic. | Daisuke Kimura, Yoshihiko Kakutani |
| 2009 | Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable. | Hongfei Fu |
| 2009 | Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine. | Yuan Dong, Kai Ren, Shengyuan Wang, Suqin Zhang |
| 2009 | A Fresh Look at Separation Algebras and Share Accounting. | Robert Dockins, Aquinas Hobor, Andrew W. Appel |
| 2009 | The Twilight Zone: From Testing to Formal Specifications and Back Again. | Koen Claessen |
| 2009 | Bi-abductive Resource Invariant Synthesis. | Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis |
| 2009 | On Stratified Regions. | Roberto M. Amadio |
| 2009 | Asymptotic Resource Usage Bounds. | Elvira Albert, Diego Esteban Alonso-Blas, Puri Arenas, Samir Genaim, German Puebla |
| 2008 | ML Modules and Haskell Type Classes: A Constructive Comparison. | Stefan Wehr, Manuel M. T. Chakravarty |
| 2008 | Interface Types for Haskell. | Peter Thiemann, Stefan Wehr |
| 2008 | Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. | Kohei Suenaga |