36. POPL 2009: Savannah, GA, USA

Invited talk

• Tim Harris:
  Language constructs for transactional memory. 1
  

Concurrency

• Tayfun Elmas, Shaz Qadeer, Serdar Tasiran:
  A calculus of atomic actions. 2-15
  
• Alexey Gotsman, Byron Cook, Matthew J. Parkinson, Viktor Vafeiadis:
  Proving that non-blocking algorithms don't block. 16-28
  
• Martín Abadi, Gordon D. Plotkin:
  A model of cooperative threads. 29-40
  

Types I

• Dana N. Xu, Simon L. Peyton Jones, Koen Claessen:
  Static contract checking for Haskell. 41-52
  
• Xin Qi, Andrew C. Myers:
  Masked types for sound object initialization. 53-65
  
• Daan Leijen:
  Flexible types: robust type inference for first-class polymorphism. 66-77
  

Medley I

• Roberto Lublinerman, Christian Szegedy, Stavros Tripakis:
  Modular code generation from synchronous block diagrams: modularity vs. code size. 78-89
  
• Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
  Formal certification of code-based cryptographic proofs. 90-101
  
• Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko:
  Verifying liveness for asynchronous programs. 102-113
  

Static analysis I

• Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, Gilles Muller:
  A foundation for flow-based program matching: using temporal logic and model checking. 114-126
  
• Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi:
  SPEED: precise and efficient static estimation of program computational complexity. 127-139
  
• David Monniaux:
  Automatic modular abstractions for linear constraints. 140-151
  

Invited talk

• Chris Barker:
  Wild control operators. 152
  

Functional programming

• Ronald Garcia, Andrew Lumsdaine, Amr Sabry:
  Lazy evaluation and delimited control. 153-164
  
• Janis Voigtländer:
  Bidirectionalization for free! (Pearl). 165-176
  
• Akimasa Morihata, Kiminori Matsuzaki, Zhenjiang Hu, Masato Takeichi:
  The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer. 177-185
  

Medley II

• Ruy Ley-Wild, Umut A. Acar, Matthew Fluet:
  A cost semantics for self-adjusting computation. 186-199
  
• Akihiko Tozawa, Michiaki Tatsubori, Tamiya Onodera, Yasuhiko Minamide:
  Copy-on-write in the PHP language. 200-212
  
• Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun:
  Feedback-directed barrier optimization in a strongly isolated STM. 213-225
  

Static analysis II

• Ben Hardekopf, Calvin Lin:
  Semi-sparse flow-sensitive pointer analysis. 226-238
  
• Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv:
  A combination framework for tracking partition sizes. 239-251
  
• Yin Wang, Stéphane Lafortune, Terence Kelly, Manjunath Kudlur, Scott A. Mahlke:
  The theory of deadlock avoidance via discrete control. 252-263
  

Static analysis III

• Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner:
  Equality saturation: a new approach to optimization. 264-276
  
• Peter A. Jonsson, Johan Nordlander:
  Positive supercompilation for a higher order call-by-value language. 277-288
  
• Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang:
  Compositional shape analysis by means of bi-abduction. 289-300
  

Invited talk

• Alex Simpson:
  Linear types for computational effects. 301
  

Program logics

• Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer:
  Unifying type checking and property checking for low-level code. 302-314
  
• Xinyu Feng:
  Local rely-guarantee reasoning. 315-327
  
• James Brotherston, Cristiano Calcagno:
  Classical BI: a logic for reasoning about dualising resources. 328-339
  

Types II

• Amal Ahmed, Derek Dreyer, Andreas Rossberg:
  State-dependent representation independence. 340-353
  
• Benoît Montagu, Didier Rémy:
  Modeling abstract types in modules with open existential types. 354-365
  
• Neelakantan R. Krishnaswami:
  Focusing on pattern matching. 366-378
  

Multicore

• Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave:
  The semantics of x86-CC multiprocessor machine code. 379-391
  
• Gérard Boudol, Gustavo Petri:
  Relaxed memory models: an operational approach. 392-403
  
• Rachid Guerraoui, Michal Kapalka:
  The semantics of progress in lock-based transactional memory. 404-415
  

Verification

• Naoki Kobayashi:
  Types and higher-order recursion schemes for verification of higher-order programs. 416-428
  
• Tom Ridge:
  Verifying distributed systems: the operational approach. 429-440
  
• Chris Hawblitzel, Erez Petrank:
  Automated verification of practical garbage collectors. 441-453