PLPV 2009: Savannah, GA, USA

• Manuel Fähndrich:
  Language-agnostic specification and verification: invited talk. 1-2
  

Session 1

• Daniel R. Licata, Robert Harper:
  Positively dependent types. 3-14
  
• Noam Zeilberger:
  Refinement types and computational duality. 15-26
  
• Kenneth W. Knowles, Cormac Flanagan:
  Compositional reasoning and decidable checking for dependent contract types. 27-38
  

Session 2

• Tom Schrijvers, Louis-Julien Guillemette, Stefan Monnier:
  Type invariants for Haskell. 39-48
  
• Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson:
  Verified programming in Guru. 49-58
  
• Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez:
  Embedding a logical theory of constructions in Agda. 59-66
  

Session 3

• Max Schäfer, Torbjörn Ekman, Oege de Moor:
  Challenge proposal: verification of refactorings. 67-72
  
• Levent Erkök, John Matthews:
  Pragmatic equivalence and safety checking in Cryptol. 73-82