| 2010 | The Audacity of Hope: Thoughts on Reclaiming the Database Dream. | Sam Lindley, Philip Wadler |
| 2010 | Deadlock-Free Channels and Locks. | K. Rustan M. Leino, Peter Mller, Jan Smans |
| 2010 | Separating Shape Graphs. | Vincent Laviron, Bor-Yuh Evan Chang, Xavier Rival |
| 2010 | On the Expressive Power of Primitives for Compensation Handling. | Ivan Lanese, Ctia Vaz, Carla Ferreira |
| 2010 | Functional Programming in Sublinear Space. | Ugo Dal Lago, Ulrich Schpp |
| 2010 | TRX: A Formally Verified Parser Interpreter. | Adam Koprowski, Henri Binsztok |
| 2010 | Automating Security Mediation Placement. | Dave King, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, Sanjit A. Seshia |
| 2010 | Generative Operational Semantics for Relaxed Memory Models. | Radha Jagadeesan, Corin Pitcher, James Riely |
| 2010 | Amortized Resource Analysis with Polynomial Potential. | Jan Hoffmann, Martin Hofmann |
| 2010 | Parameterized Memory Models and Concurrent Separation Logic. | Rodrigo Ferreira, Xinyu Feng, Zhong Shao |
| 2010 | Propositional Interpolation and Abstract Interpretation. | Vijay D'Silva |
| 2010 | Fluid Updates: Beyond Strong vs. Weak Updates. | Isil Dillig, Thomas Dillig, Alex Aiken |
| 2010 | Logical Concurrency Control from Sequential Proofs. | Jyotirmoy V. Deshmukh, G. Ramalingam, Venkatesh Prasad Ranganath, Kapil Vaswani |
| 2010 | A Theory of Speculative Computation. | Grard Boudol, Gustavo Petri |
| 2010 | Formal Verification of Coalescing Graph-Coloring Register Allocation. | Sandrine Blazy, Benot Robillard, Andrew W. Appel |
| 2010 | Testing Polymorphic Properties. | Jean-Philippe Bernardy, Patrik Jansson, Koen Claessen |
| 2010 | A PolyTime Functional Language from Light Linear Logic. | Patrick Baillot, Marco Gaboardi, Virgile Mogbil |
| 2010 | Amortised Resource Analysis with Separation Logic. | Robert Atkey |
| 2010 | A Semantic Framework for Declassification and Endorsement. | Aslan Askarov, Andrew C. Myers |
| 2010 | Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays. | Torben Amtoft, John Hatcliff, Edwin Rodrguez |
| 2010 | Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis. | Assal Adj, Stphane Gaubert, Eric Goubault |
| 2009 | An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees. | Hao Yuan, Patrick Th. Eugster |
| 2009 | Well-Typed Programs Can't Be Blamed. | Philip Wadler, Robert Bruce Findler |
| 2009 | A Theory of Non-monotone Memory (Or: Contexts for free). | Eijiro Sumii |
| 2009 | Practical Variable-Arity Polymorphism. | T. Stephen Strickland, Sam Tobin-Hochstadt, Matthias Felleisen |