| 2009 | A Basis for Verifying Multi-threaded Programs. K. Rustan M. Leino, Peter Müller |
| 2009 | A Theory of Non-monotone Memory (Or: Contexts for free). Eijiro Sumii |
| 2009 | Abstract Processes in Orchestration Languages. Maria Grazia Buscemi, Hernán C. Melgratti |
| 2009 | Abstraction for Concurrent Objects. Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang |
| 2009 | All Secrets Great and Small. Delphine Demange, David Sands |
| 2009 | Amortised Memory Analysis Using the Depth of Data Structures. Brian Campbell |
| 2009 | An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees. Hao Yuan, Patrick Th. Eugster |
| 2009 | An Interval-Based Inference of Variant Parametric Types. Florin Craciun, Wei-Ngan Chin, Guanhua He, Shengchao Qin |
| 2009 | Automatic Parallelization with Separation Logic. Mohammad Raza, Cristiano Calcagno, Philippa Gardner |
| 2009 | Conversation Types. Luís Caires, Hugo Torres Vieira |
| 2009 | Deny-Guarantee Reasoning. Mike Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis |
| 2009 | Existential Quantification for Variant Ownership. Nicholas Cameron, Sophia Drossopoulou |
| 2009 | Exploring the Design Space of Higher-Order Casts. Jeremy G. Siek, Ronald Garcia, Walid Taha |
| 2009 | Formalising and Verifying Reference Attribute Grammars in Coq. Max Schäfer, Torbjörn Ekman, Oege de Moor |
| 2009 | Global Principal Typing in Partially Commutative Asynchronous Sessions. Dimitris Mostrous, Nobuko Yoshida, Kohei Honda |
| 2009 | Handlers of Algebraic Effects. Gordon D. Plotkin, Matija Pretnar |
| 2009 | Is Structural Subtyping Useful? An Empirical Study. Donna Malayeri, Jonathan Aldrich |
| 2009 | Minimization Algorithm for Symbolic Bisimilarity. Filippo Bonchi, Ugo Montanari |
| 2009 | Modular Monad Transformers. Mauro Jaskelioff |
| 2009 | Practical Variable-Arity Polymorphism. T. Stephen Strickland, Sam Tobin-Hochstadt, Matthias Felleisen |
| 2009 | Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings Giuseppe Castagna |
| 2009 | Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. Matthew R. Lakin, Andrew M. Pitts |
| 2009 | SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs. Caitlin Sadowski, Stephen N. Freund, Cormac Flanagan |
| 2009 | The Financial Crisis, a Lack of Contract Specification Tools: What Can Finance Learn from Programming Language Design?. Jean-Marc Eber |
| 2009 | Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. Hridesh Rajan, Jia Tao, Steve M. Shaner, Gary T. Leavens |
| 2009 | Type-Based Automated Verification of Authenticity in Cryptographic Protocols. Daisuke Kikuchi, Naoki Kobayashi |
| 2009 | Using Category Theory to Design Programming Languages. John C. Reynolds |
| 2009 | Verified, Executable Parsing. Aditi Barthwal, Michael Norrish |
| 2009 | Well-Typed Programs Can't Be Blamed. Philip Wadler, Robert Bruce Findler |