WEDNESDAY, January 21, 2009
Invited talk 9:00-10:00 (Session chair: Benjamin C. Pierce, University of Pennsylvania)
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)
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)
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