37. POPL 2010: Madrid, Spain

Invited talk

• Neil Gershenfeld, David Dalrymple, Kailiang Chen, Ara Knaian, Forrest Green, Erik D. Demaine, Scott Greenwald, Peter Schmidt-Nielsen:
  Reconfigurable asynchronous logic automata: (RALA). 1-6
  

Concurrency

• Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi:
  On the verification problem for weak memory models. 7-18
  
• Eric Koskinen, Matthew Parkinson, Maurice Herlihy:
  Coarse-grained transactions. 19-30
  
• Hagit Attiya, G. Ramalingam, Noam Rinetzky:
  Sequential verification of serializability. 31-42
  

Static analysis I

• Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali:
  Compositional may-must program analysis: unleashing the power of alternation. 43-56
  
• Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman:
  Continuity analysis of programs. 57-70
  
• William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta:
  Program analysis via satisfiability modulo path programs. 71-82
  

Verified compilers

• Jean-Baptiste Tristan, Xavier Leroy:
  A simple, verified validator for software pipelining. 83-92
  
• Adam J. Chlipala:
  A verified compiler for an impure functional language. 93-106
  
• Magnus O. Myreen:
  Verified just-in-time compiler on x86. 107-118
  

Type inference

• Tachio Terauchi:
  Dependent types from counterexamples. 119-130
  
• Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala:
  Low-level liquid types. 131-144
  
• Max Schäfer, Oege de Moor:
  Type inference for datalog with complex type hierarchies. 145-156
  

Invited talk

• Thomas A. Henzinger:
  From Boolean to quantitative notions of correctness. 157-158
  

Reasoning about programs

• Andrew M. Pitts:
  Nominal system T. 159-170
  
• Aquinas Hobor, Robert Dockins, Andrew W. Appel:
  A theory of indirection via approximation. 171-184
  
• Derek Dreyer, Georg Neis, Andreas Rossberg, Lars Birkedal:
  A relational modal logic for higher-order stateful ADTs. 185-198
  

Static analysis II

• Philippe Suter, Mirco Dotta, Viktor Kuncak:
  Decision procedures for algebraic data types with abstractions. 199-210
  
• Stephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay:
  Automatic numeric abstractions for heap-manipulating programs. 211-222
  
• Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann:
  Static determination of quantitative resource usage for higher-order programs. 223-236
  

Verification

• J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky:
  Toward a verified relational database management system. 237-248
  
• Andreas Podelski, Thomas Wies:
  Counterexample-guided focus. 249-260
  
• Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine:
  Structuring the verification of heap-manipulating programs. 261-274
  

Types

• Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich:
  Dependent types and program equivalence. 275-286
  
• DeLesley S. Hutchins:
  Pure subtype systems. 287-298
  
• Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, Alexandre Z. Caldeira:
  Modular session types for distributed object-oriented programming. 299-312
  

Program synthesis

• Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster:
  From program verification to program synthesis. 313-326
  
• Martin T. Vechev, Eran Yahav, Greta Yorsh:
  Abstraction-guided synthesis of synchronization. 327-338
  
• Rastislav Bodík, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, Casey Rodarmor:
  Programming with angelic nondeterminism. 339-352
  

Relating and integrating static and dynamic checks

• Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich:
  Contracts made manifest. 353-364
  
• Jeremy G. Siek, Philip Wadler:
  Threesomes, with and without blame. 365-376
  
• Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, Jan Vitek:
  Integrating typed and untyped code in a scripting language. 377-388
  

Compilers

• Ross Tate, Michael Stepp, Sorin Lerner:
  Generating compiler optimizations from proofs. 389-402
  
• João Dias, Norman Ramsey:
  Automatically generating instruction selectors using declarative machine descriptions. 403-416
  
• Trevor Jim, Yitzhak Mandelbaum, David Walker:
  Semantics and algorithms for data-dependent grammars. 417-430
  

Security and ownership

• Niklas Broberg, David Sands:
  Paralocks: role-based information flow control and beyond. 431-444
  
• Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
  Modular verification of security protocol code by typing. 445-456
  
• Jean-Phillipe Martin, Michael Hicks, Manuel Costa, Periklis Akritidis, Miguel Castro:
  Dynamically checking ownership policies in concurrent c/c++ programs. 457-470
  

Medley

• Matthias Heizmann, Jochen Hoenicke, Andreas Podelski:
  Nested interpolants. 471-482
  
• Andrzej Filinski:
  Monads in action. 483-494
  
• Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno:
  Higher-order multi-parameter tree transducers and recursion schemes for program verification. 495-508