[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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