WEDNESDAY, January 21, 2009

Invited talk 9:00-10:00 (Session chair: Benjamin C. Pierce, University of Pennsylvania)

Tim Harris, Microsoft Research, UK

Concurrency   10:30-11:30 (Session chair: Antony Hosking, Purdue University)

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

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

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

Types I   12:00-1:00 (Session chair: James Cheney, University of Edinburgh)

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

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

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

Medley I   2:30-3:30 (Session chair: Frank Pfenning, CMU, USA)

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

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

Static Analysis I   4:00-5:00 (Session chair: Jens Palsberg, UCLA, USA)

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

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

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

Panel: Grand Challenges in Programming Languages   5:15 - 6:15

(Session chair: Andrew Appel, Princeton, USA)

Programming languages are pervasive in every area of computer science, and the formalisms behind programming languages are as old as computer science itself. Nonetheless, mainstream computer scientists often have difficulty understanding the motivation for PL research... what are the big, difficult, concrete, and practical challenges in computer science that PL research can help address? This panel brings together experts in the field to discuss potential answers.

    Kathryn McKinley, University of Texas at Austin, USA
    Greg Morrisett, Harvard University, USA
    Xavier Leroy, INRIA, France
    Simon Peyton-Jones, Microsoft Research, UK
    Martin Rinard, MIT, USA

THURSDAY, January 22, 2009

Invited talk   9:00-10:00 (Session chair: Mitchell Wand, Northeastern University, USA)

Chris Barker, NYU, USA

Functional Programming   10:30-11:30 (Session chair: Patricia Johann, University of Strathclyde)

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

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

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

Medley II   12:00-1:00 (Session chair: Martin Hofmann, LMU, Munich, Germany)

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

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

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

Static Analysis II   2:30-3:30 (Session chair: Michael Hicks, University of Maryland, College Park)

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

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
    Stephane Lafortune, Discrete Event Systems Lab, U. Michigan EECS
    Terence Kelly, HP Labs
    Manjunath Kudlur, Advanced Computer Architecture Lab, U. Michigan EECS
    Scott Mahlke, Advanced Computer Architecture Lab, U. Michigan EECS

Static Analysis III   4:00-5:00 (Session chair: Anindya Banerjee, Kansas State University and IMDEA-SW, Madrid)

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

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

Compositional Shape Analysis by means of Bi-Abduction
    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

Program Chair's report and announcement of POPL 2010, 5:00 - 5:30

    Benjamin C. Pierce, University of Pennsylvania, USA
    Manuel Hermenegildo, IMDEA-Software and T.U. of Madrid, Spain
    Jens Palsberg, UCLA, USA

FRIDAY, January 23, 2009

Invited talk   9:00-10:00 (Session chair: Masahito Hasegawa, Kyoto University)

Alex Simpson, University of Edinburgh, UK

Program Logics   10:30-11:30 (Session chair: Nick Benton, Microsoft Research)

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

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

Types II   12:00-1:00 (Session chair: Atsushi Igarashi, Kyoto University)

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

Modeling Abstract Types in Modules with Open Existential Types
    Benoit Montagu, INRIA
    Didier Remy, INRIA

Focusing on Pattern Matching
    Neelakantan Krishnaswami, Carnegie Mellon University

Multicore   2:30-3:30 (Session chair: Leaf Petersen, Intel Corporation)

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

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

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

Verification   4:00-5:00 (Session chair: Andrew Appel, Princeton University, USA)

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

Verifying Distributed Systems: the Operational Approach
    Tom Ridge, University of Cambridge

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