35. POPL 2008: San Francisco, California, USA

George C. Necula, Philip Wadler (Eds.): Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008. ACM 2008, ISBN 978-1-59593-689-9 BibTeX

Session 1

Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, Stephanie Weirich:
Engineering formal metatheory. 3-15
Electronic Edition (ACM DL) BibTeX
Jean-Baptiste Tristan, Xavier Leroy:
Formal verification of translation validators: a case study on instruction scheduling optimizations. 17-27
Electronic Edition (ACM DL) BibTeX
Janis Voigtländer:
Much ado about two (pearl): a pearl on parallel prefix computation. 29-35
Electronic Edition (ACM DL) BibTeX

Session 2

Iulian Neamtiu, Michael Hicks, Jeffrey S. Foster, Polyvios Pratikakis:
Contextual effects for version-consistent dynamic software updatingalland safe concurrent programming. 37-49
Electronic Edition (ACM DL) BibTeX
Katherine F. Moore, Dan Grossman:
High-level small-step operational semantics for transactions. 51-62
Electronic Edition (ACM DL) BibTeX
Martín Abadi, Andrew Birrell, Tim Harris, Michael Isard:
Semantics of transactional memory and automatic mutual exclusion. 63-74
Electronic Edition (ACM DL) BibTeX

Session 3

Matthew J. Parkinson, Gavin M. Bierman:
Separation logic, abstraction and inheritance. 75-86
Electronic Edition (ACM DL) BibTeX
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin:
Enhancing modular OO verification with separation logic. 87-99
Electronic Edition (ACM DL) BibTeX
James Brotherston, Richard Bornat, Cristiano Calcagno:
Cyclic proofs of program termination in separation logic. 101-112
Electronic Edition (ACM DL) BibTeX

Session 4

Andrea Asperti:
The intensional content of Rice's theorem. 113-119
Electronic Edition (ACM DL) BibTeX
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca:
A logical account of pspace. 121-131
Electronic Edition (ACM DL) BibTeX
Nils Anders Danielsson:
Lightweight semiformal time complexity analysis for purely functional data structures. 133-144
Electronic Edition (ACM DL) BibTeX

Session 5

Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, Ru-Gang Xu:
Proving non-termination. 147-158
Electronic Edition (ACM DL) BibTeX
Swarat Chaudhuri:
Subcubic algorithms for recursive state machines. 159-169
Electronic Edition (ACM DL) BibTeX
Shuvendu K. Lahiri, Shaz Qadeer:
Back to the future: revisiting precise program verification using SMT solvers. 171-182
Electronic Edition (ACM DL) BibTeX

Session 6

Christopher Unkel, Monica S. Lam:
Automatic inference of stationary fields: a generalization of java's final fields. 183-195
Electronic Edition (ACM DL) BibTeX
Xin Zheng, Radu Rugina:
Demand-driven alias analysis for C. 197-208
Electronic Edition (ACM DL) BibTeX
Marius Nita, Dan Grossman, Craig Chambers:
A theory of platform-dependent low-level software. 209-220
Electronic Edition (ACM DL) BibTeX

Session 7

Greta Yorsh, Eran Yahav, Satish Chandra:
Generating precise and concise procedure summaries. 221-234
Electronic Edition (ACM DL) BibTeX
Sumit Gulwani, Bill McCloskey, Ashish Tiwari:
Lifting abstract interpreters to quantified logical domains. 235-246
Electronic Edition (ACM DL) BibTeX
Bor-Yuh Evan Chang, Xavier Rival:
Relational inductive shape analysis. 247-260
Electronic Edition (ACM DL) BibTeX

Session 8

Giuseppe Castagna, Nils Gesbert, Luca Padovani:
A theory of contracts for web services. 261-272
Electronic Edition (ACM DL) BibTeX
Kohei Honda, Nobuko Yoshida, Marco Carbone:
Multiparty asynchronous session types. 273-284
Electronic Edition (ACM DL) BibTeX

Session 9

Conor McBride:
Clowns to the left of me, jokers to the right (pearl): dissecting data structures. 287-295
Electronic Edition (ACM DL) BibTeX
Patricia Johann, Neil Ghani:
Foundations for structured programming with GADTs. 297-308
Electronic Edition (ACM DL) BibTeX
Umut A. Acar, Amal Ahmed, Matthias Blume:
Imperative self-adjusting computation. 309-322
Electronic Edition (ACM DL) BibTeX

Session 10

Cédric Fournet, Tamara Rezk:
Cryptographically sound implementations for typed information-flow security. 323-335
Electronic Edition (ACM DL) BibTeX
Peeter Laud:
On the computational soundness of cryptographically masked flows. 337-348
Electronic Edition (ACM DL) BibTeX
Hamed Seiied Alavi, Seth Gilbert, Rachid Guerraoui:
Extensible encoding of type hierarchies. 349-358
Electronic Edition (ACM DL) BibTeX

Session 11

Noam Zeilberger:
Focusing and higher-order abstract syntax. 359-369
Electronic Edition (ACM DL) BibTeX
Brigitte Pientka:
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. 371-382
Electronic Edition (ACM DL) BibTeX
Hugo Herbelin, Silvia Ghilezan:
An approach to call-by-name delimited continuations. 383-394
Electronic Edition (ACM DL) BibTeX

Session 12

Sam Tobin-Hochstadt, Matthias Felleisen:
The design and implementation of typed scheme. 395-406
Electronic Edition (ACM DL) BibTeX
Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, Alan Schmitt:
Boomerang: resourceful lenses for string data. 407-419
Electronic Edition (ACM DL) BibTeX
Kathleen Fisher, David Walker, Kenny Qili Zhu, Peter White:
From dirt to shovels: fully automatic tool generation from ad hoc data. 421-434
Electronic Edition (ACM DL) BibTeX
Walter Fontana:
Systems biology, models, and concurrency. 1-2
Electronic Edition (ACM DL) BibTeX
Kenneth L. McMillan:
Relevance heuristics for program analysis. 145-146
Electronic Edition (ACM DL) BibTeX
Yaron Minsky:
Caml trading. 285
Electronic Edition (ACM DL) BibTeX