The Coq mailing list

[Zhong Shao <shao AT cs.yale.edu>]

********************************************************************* 
* ACM SIGPLAN-SIGACT Symposium                                      * 
* on                                                                * 
* Principles of Programming Languages                               * 
*                                                                   * 
* January 21-23, 2009                                               * 
* Savannah, Georgia, USA                                            * 
*                                                                   * 
* Call for Participation                                            * 
*                                                                   * 
* http://www.cs.ucsd.edu/popl/09                                    * ;
********************************************************************* 

Important dates 

* Hotel reservation deadline: December 18, 2008 
* Early registration deadline: December 19, 2008 
* Conference: January 21-23, 2009 

Hotel 

All the conference events will take place at the Hyatt Regency 
Savannah. We encourage attendees to stay at the conference 
hotel. Information about the hotel can be found on the POPL web page: 

http://www.cs.ucsd.edu/popl/09/ ;

Scope 

The annual Symposium on Principles of Programming Languages is a 
forum for the discussion of fundamental principles and important 
innovations in the design, definition, analysis, transformation, 
implementation and verification of programming languages, programming 
systems, and programming abstractions. Both experimental and 
theoretical papers are welcome. 

Preliminary Program 

A preliminary program can be found at the end of this email in text 
format, or it can be found here: 

http://www.cs.ucsd.edu/popl/09/program.html ;

Program Highlights 

Invited speakers: 
* Tim Harris, Microsoft Research, UK 
* Chris Barker, NYU, USA 
* Alex Simpson, University of Edinburgh, UK 

Panel: Grand Challenges in Programming Languages 
* 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 

Student Attendees 

Students who have a paper accepted for the conference are offered 
SIGPLAN student membership free for one year. As members of SIGPLAN 
they may apply for travel fellowships from the PAC fund 
( http://www.acm.org/sigs/sigplan/PAC.htm ;). 



General Chair: 
Zhong Shao 
Department of Computer Science 
Yale University 

Program Chair: 
Benjamin C. Pierce 
Department of Computer & Information Science 
University of Pennsylvania 

Program Committee: 
Andrew Appel Princeton University 
Anindya Banerjee Kansas State University 
Nick Benton Microsoft 
Bruno Blanchet CNRS, Ecole Normale Superieure & INRIA 
James Cheney Edinburgh University 
Matthew Flatt University of Utah 
Giorgio Ghelli University of Pisa 
Masahito Hasegawa Kyoto University 
Hugo Herbelin INRIA 
Michael Hicks University of Maryland, College Park 
Martin Hofmann Ludwig-Maximilians-Universitt Munich 
Susan Horwitz University of Wisconsin 
Tony Hosking Purdue University 
John Hughes Chalmers University of Technology 
Atsushi Igarashi Kyoto University 
Patricia Johann Rutgers University 
James Leifer INRIA 
Jens Palsberg UCLA 
Leaf Petersen Intel 
Frank Pfenning Carnegie Mellon University 
Benjamin Pierce University of Pennsylvania 
Sriram Rajamani Microsoft 
David Sands Chalmers University of Technology 
Guy Steele Sun Microsystems 
Mitch Wand Northeastern University 



Affiliated Events 

(more details here: http://www.cs.ucsd.edu/popl/09/#AffiliatedEvents ;) 

* DAMP: Declarative Aspects of Multicore Programming 
* January 20, 2009 

* PLPV: Programming Languages meets Program Verification 
* January 20, 2009 

* FOOL: Foundations of Object-Oriented Languages 
* January 24, 2009 

* PADL: Practical Applications of Declarative Languages 
* January 19-20, 2009 

* PEPM: Partial Evaluation and Semantics-Based Program Manipulation 
* January 19-20, 2009 

* PLAN-X: Programming Language Technologies for XML 
* January 24, 2009 

* TLDI:Types in Language Design and Implementation 
* January 24, 2009 

* Twelf tutorial: Mechanizing Metatheory with LF and Twelf 
* January 19, 2009 

* VMCAI:Verification Model Checking and Abstract Interpretation 
* January 18-20, 2009 



Preliminary Program 

* WEDNESDAY, January 21, 2009 

** Invited talk: Tim Harris, Microsoft Research, UK 
(Session chair: Benjamin C. Pierce, University of Pennsylvania) 
9:00 - 10:00 

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

*** 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 (Session chair: James Cheney, University of Edinburgh) 
12:00 - 1:00 

*** 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 (Session chair: Frank Pfenning, CMU, USA) 
2:30 - 3:30 

*** 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 (Session chair: Jens Palsberg, UCLA, USA) 
4:00 - 5:00 

*** 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 

*** 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 University, USA) 
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: Chris Barker, NYU, USA 
(Session chair: Mitchell Wand, Northeastern University, USA) 
9:00 - 10:00 

------------------- 
** FUNCTIONAL PROGRAMMING 
(Session chair: Patricia Johann, University of Strathclyde) 
10:30 - 11:30 

*** 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 (Session chair: Martin Hofmann, LMU, Munich, Germany) 
12:00 - 1:00 


*** 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 
(Session chair: Michael Hicks, University of Maryland, College Park) 
2:30 - 3:30 

*** 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 
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 

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

*** 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: Alex Simpson, University of Edinburgh, UK 
(Session chair: Masahito Hasegawa, Kyoto University) 
9:00 - 10:00 

------------------- 
** PROGRAM LOGICS (Session chair: Nick Benton, Microsoft Research) 
10:30 - 11:30 

*** 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 (Session chair: Atsushi Igarashi, Kyoto University) 
12:00 - 1:00 

*** 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 (Session chair: Leaf Petersen, Intel Corporation) 
2:30 - 3:30 

*** 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 (Session chair: Andrew Appel, Princeton University, USA) 
4:00 - 5:00 

*** 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 

______________________________________________________________________________