Accepted Papers

Brigitte Pientka
Functional programming with higher-order abstract syntax and explicit substitution

Adam Chlipala
Position Paper: Thoughts on Programming with Proof Assistants

Tim Sheard
Type-level Computation Using Narrowing in Omega

James Caldwell, Josef Pohl
Constructive membership predicates as index types

Andreas Schlosser, Christoph Walther, Michael Gonder, and Markus Aderhold
Context-Dependent Procedures and Computed Types in VeriFun

Oleg Kiselyov, Chung-chieh Shan
Lightweight static capabilities

Louis-Julien Guillemette, Stefan Monnier
Statically Verified Type-Preserving Code Transformations in Haskell

Aaron Stump
The Alternation Calculus

Martin Sulzmann, Razvan Voicu
Language-Based Program Verification via Expressive Types