POPL 09 accepted papers and their link

Automatic modular abstractions for linear constraints
  David Monniaux, CNRS / VERIMAG

Static Contract Checking for Haskell  ppt
  Dana N. Xu, University of Cambridge,
  Simon Peyton Jones, Microsoft Research
  Koen Claessen, Chalmers University of Technology

Proving that non-blocking algorithms don't block ppt
  Alexey Gotsman, University of Cambridge
  Byron Cook, Microsoft Research
  Matthew Parkinson, University of Cambridge
  Viktor Vafeiadis, Microsoft Research

Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs
  Naoki Kobayashi, Tohoku University

Compositional Shape Analysis
  Cristiano Calcagno, Imperial College, London
  Dino Distefano, Queen Mary, University of London
  Peter O'Hearn, Queen Mary, University of London
  Hongseok Yang, Queen Mary, University of London

Semi-Sparse Flow-Sensitive Pointer Analysis
  Ben Hardekopf, The University of Texas at Austin
  Calvin Lin, The University of Texas at Austin

Feedback-Directed Barrier Optimization in a Strongly Isolated STM
  Nathan Bronson, Stanford CS
  Christos Kozyrakis, Stanford CS
  Kunle Olukotun, Stanford CS

Modular Code Generation from Synchronous Block Diagrams: Modularity vs. Code Size
  Roberto Lublinerman, The Pennsylvania State University
  Christian Szegedy, Cadence Research Laboratories
  Stavros Tripakis, Cadence Research Laboratories

Formal Certification of Code-Based Cryptographic Proofs
  Gilles Barthe, IMDEA Software, Madrid and Microsoft Research - INRIA Joint Centre
  Benjamin Gregoire, INRIA Sophia Antipolis and Microsoft Research - INRIA Joint Centre
  Santiago Zanella, INRIA Sophia Antipolis and Microsoft Research - INRIA Joint Centre

Relaxed memory models: an operational approach
  Gerard Boudol, INRIA Sophia Antipolis
  Gustavo Petri, INRIA Sophia Antipolis

Bidirectionalization for Free! (Pearl)
  Janis Voigtlander, Technische Universitat Dresden

The Semantics of x86 Multiprocessor Machine Code
  Susmit Sarkar, University of Cambridge
  Peter Sewell, University of Cambridge
  Francesco Zappa Nardelli, INRIA
  Scott Owens, University of Cambridge
  Thomas Braibant, INRIA
  Magnus Myreen, University of Cambridge
  Jade Alglave, INRIA

Flexible types: Robust type inference for first-class polymorphism
  Daan Leijen, Microsoft Research

Verifying Liveness for Asynchronous Programs
  Pierre Ganty, UC Los Angeles
  Rupak Majumdar, UC Los Angeles
  Andrey Rybalchenko, MPI SWS

Masked types for sound object initialization
  Xin Qi, Cornell University
  Andrew C. Myers, Cornell University

A Model of Cooperative Threads
  Martin Abadi, Microsoft and UCSC
  Gordon Plotkin, University of Edinburgh and Microsoft

State-Dependent Representation Independence
  Amal Ahmed, TTI-C
  Derek Dreyer, MPI-SWS
  Andreas Rossberg, MPI-SWS

Equality Saturation: a new Approach to Optimization
  Ross Tate, UC San Diego
  Michael Stepp, UC San Diego
  Zachary Tatlock, UC San Diego
  Sorin Lerner, UC San Diego

The Semantics of Progress in Lock-Based Transactional Memory
  Rachid Guerraoui, EPFL
  Michal Kapalka, EPFL

Positive Supercompilation for a higher order call-by-value language
  Peter A. Jonsson, Lulea University of Technology
  Johan Nordlander, Lulea University of Technology

Unifying Type Checking and Property Checking for Low-Level Code
  Jeremy Condit, Microsoft Research
  Brian Hackett, Stanford University
  Shuvendu Lahiri, Microsoft Research
  Shaz Qadeer, Microsoft Research

The Third Homomorphism Theorem on Trees: Downward & Upward Lead to Divide-and-Conquer
  Akimasa Morihata, University of Tokyo
  Kiminori Matsuzaki, University of Tokyo
  Zhenjiang Hu, National Institute of Informatics
  Masato Takeichi, University of Tokyo

On verifying enterprise infrastructure
  Tom Ridge, University of Cambridge

A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
  Julien Brunel, DIKU, University of Copenhagen
  Damien Doligez, INRIA, Gallium Project
  Rene Rydhof Hansen, Aalborg University
  Julia L. Lawall, DIKU, University of Copenhagen
  Gilles Muller, Ecole des Mines de Nantes

A Calculus of Atomic Actions
  Tayfun Elmas, Koc University
  Shaz Qadeer, Microsoft Research
  Serdar Tasiran, Koc University

Copy-on-Write in the PHP Language
  Akihiko Tozawa, IBM Tokyo Research Lab.
  Michiaki Tatsubori, IBM Tokyo Research Lab.
  Tamiya Onodera, IBM Tokyo Research Lab.
  Yasuhiko Minamide, Tsukuba University

Local Rely-Guarantee Reasoning
  Xinyu Feng, Toyota Technological Institute at Chicago

Classical BI (A Logic for Reasoning about Dualising Resource)
  James Brotherston, Imperial College London
  Cristiano Calcagno, Imperial College London

Why are open existential types are so good?
  Benoit Montagu, INRIA
  Didier Remy, INRIA

Lazy Evaluation and Delimited Control
  Ronald Garcia, Indiana University
  Andrew Lumsdaine, Indiana University
  Amr Sabry, Indiana University

Automated Verification of Practical Garbage Collectors
  Chris Hawblitzel, Microsoft Research
  Erez Petrank, Microsoft Research

A Combination Framework for Tracking Partition Sizes
  Sumit Gulwani, Microsoft Research
  Tal Lev-Ami, Tel-Aviv University
  Mooly Sagiv, Tel-Aviv University

The Theory of Deadlock Avoidance via Discrete Control
  Yin Wang, Discrete Event Systems Lab, U. Michigan EECS
  Scott Mahlke, Advanced Computer Architecture Lab, U. Michigan EECS
  Stephane Lafortune, Discrete Event Systems Lab, U. Michigan EECS
  Terence Kelly, HP Labs
  Manjunath Kudlur, Advanced Computer Architecture Lab, U. Michigan EECS

SPEED: Precise and Efficient Static Estimation of Program Computational Complexity
  Sumit Gulwani, Microsoft Research
  Krishna Mehra, Microsoft Research
  Trishul Chilimbi, Microsoft Research

A Cost Semantics for Self-Adjusting Computation
  Ruy Ley Wild, Carnegie Mellon University
  Umut A. Acar, Toyota Technological Institute
  Matthew Fluet, Toyota Technological Institute

Focusing on Pattern Matching
  Neelakantan Krishnaswami, Carnegie Mellon University