Workshop Schedule, 20 January, 2009:

09:00-10:00 Invited Talk

Language-Agnostic Specification and Verification.Manuel Fähndrich
10:00-10:30 break
10:30-12:00 Session I

Positively Dependent Types.Daniel R. Licata and Robert Harper.
Refinement Types and Computational Duality. Noam Zeilberger.
Compositional and Decidable Checking for Dependent Contract Types. Kenneth Knowles and Cormac Flanagan.
12:00-13:30 lunch
13:30-15:00 Session II

Type Invariants for Haskell.Tom Schrijvers Louis-Julien Guillemette and Stefan Monnier.
Verified Programming in Guru. Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller and Timothy Simpson .
Embedding a Logical Theory of Constructions in Agda. Ana Bove, Peter Dybjer and Andrés Sicard Ramírez
15:00-15:30 break
15:30-16:35 Session III

Challenge Proposal: Verification of Refactorings.Max Schaefer, Torbjörn Ekman and Oege de Moor
Pragmatic equivalence and safety checking in Cryptol. Levent Erkok and John Matthews
16:30-17:30 Discussion