TLDI 2009: Savannah, GA, USA

• Ulf Norell:
  Dependently typed programming in Agda. 1-2
  

Session 1

• Nick Benton, Nicolas Tabareau:
  Compiling functional types to relational specifications for low level imperative code. 3-14
  
• Arthur I. Baars, S. Doaitse Swierstra, Marcos Viera:
  Typed transformations of typed abstract syntax. 15-26
  
• Ioannis G. Baltopoulos, Andrew D. Gordon:
  Secure compilation of a multi-tier web language. 27-38
  

Session 2

• Daniel Marino, Todd D. Millstein:
  A generic type-and-effect system. 39-50
  
• Marwan Abi-Antoun, Jonathan Aldrich:
  Static extraction of sound hierarchical runtime object graphs. 51-64
  
• Pierre-Évariste Dagand, Dejan Kostic, Viktor Kuncak:
  Opis: reliable distributed systems in OCaml. 65-78
  

Session 3

• Aleksandar Nanevski, Paul Govereau, Greg Morrisett:
  Towards type-theoretic semantics for transactional concurrency. 79-90
  
• Lars Birkedal, Kristian Støvring, Jacob Thamsborg:
  Relational parametricity for references and recursive types. 91-104
  
• Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse:
  Design patterns in separation logic. 105-116