[TYPES/announce] POPL 2009 accepted papers

[Benjamin Pierce]

I am delighted to announce that the following papers have been  
accepted for presentation at POPL 2009 (Jan 21-23 in Savannah,  
Georgia, USA, http://www.cs.ucsd.edu/popl/09).

Hope to see you there!

      - Benjamin



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

Static Contract Checking for Haskell
   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
   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
   René 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
   Trishul Chilimbi, Microsoft Research
   Krishna Mehra, 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