36. POPL 2009: Savannah, GA, USA

Zhong Shao, Benjamin C. Pierce (Eds.): Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM 2009, ISBN 978-1-60558-379-2 BibTeX

Invited talk

Tim Harris:
Language constructs for transactional memory. 1
Electronic Edition (ACM DL) BibTeX

Concurrency

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

Types I

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

Medley I

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

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
Electronic Edition (ACM DL) BibTeX
Sumit Gulwani, Krishna K. Mehra, Trishul M. Chilimbi:
SPEED: precise and efficient static estimation of program computational complexity. 127-139
Electronic Edition (ACM DL) BibTeX
David Monniaux:
Automatic modular abstractions for linear constraints. 140-151
Electronic Edition (ACM DL) BibTeX

Invited talk

Chris Barker:
Wild control operators. 152
Electronic Edition (ACM DL) BibTeX

Functional programming

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

Medley II

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

Static analysis II

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

Static analysis III

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

Invited talk

Alex Simpson:
Linear types for computational effects. 301
Electronic Edition (ACM DL) BibTeX

Program logics

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

Types II

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

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
Electronic Edition (ACM DL) BibTeX
Gérard Boudol, Gustavo Petri:
Relaxed memory models: an operational approach. 392-403
Electronic Edition (ACM DL) BibTeX
Rachid Guerraoui, Michal Kapalka:
The semantics of progress in lock-based transactional memory. 404-415
Electronic Edition (ACM DL) BibTeX

Verification

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