35. POPL 2008: San Francisco, California, USA

Session 1

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

Session 2

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

Session 3

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

Session 4

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

Session 5

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

Session 6

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

Session 7

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

Session 8

• Giuseppe Castagna, Nils Gesbert, Luca Padovani:
  A theory of contracts for web services. 261-272
  
• Kohei Honda, Nobuko Yoshida, Marco Carbone:
  Multiparty asynchronous session types. 273-284
  

Session 9

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

Session 10

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

Session 11

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

Session 12

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