Program

All sessions will take place in Richmond unless otherwise indicated.

Monday, August 21st

Monday's program is also available with abstracts or side by side with other meetings.

09:00‑10:30  Session 1: Martin-Loef Type Theory

09:00	Peter Dybjer (Chalmers University of Technology) Programming Languages Meet Program Verification [pdf]
10:00	James Caldwell and Josef Pohl Constructive membership predicates as index types

10:30‑11:00  Break

11:00‑12:30  Session 2: Verified Programming in Haskell

11:00	Martin Sulzmann and Razvan Voicu Language-Based Program Verification via Expressive Types
11:30	Oleg Kiselyov and Chung-chieh Shan Lightweight static capabilities
12:00	Louis-Julien Guillemette and Stefan Monnier Statically Verified Type-Preserving Code Transformations in Haskell

12:30‑14:00  Lunch break

14:00‑15:30  Session 3: Verification Environments

14:00	Tim Sheard Type-level Computation Using Narrowing in Omega
14:30	Andreas Schlosser , Christoph Walther , Michael Gonder and Markus Aderhold Context-Dependent Procedures and Computed Types in VeriFun
15:00	Brigitte Pientka Functional programming with higher-order abstract syntax and explicit substitution

15:30‑16:00  Break

16:00‑16:30  Session 4: Short Papers

16:00	Aaron Stump The Alternation Calculus
16:15	Adam Chlipala Position Paper: Thoughts on Programming with Proof Assistants

16:30‑17:15  Panel Discussion: Future Directions of Language-Based Program Verification