09:00-10:00 |
Invited Talk (Chair: Hongwei Xi) Jessie: an Intermediate Language for Java and C Verification. Claude Marche. |
10:00-10:30 | coffee |
10:30-12:00 |
Session I: Monads, Refinement (Chair: Stefan Monnier)
Compound Monads in Specification Languages. Jeremy Dawson. A Coinductive Monad for Prop-Bounded Recursion. Adam Megacz. Refined typechecking with Stardust. Joshua Dunfield. |
12:00-14:00 | lunch |
14:00-15:30 |
Session II: Low-level Types, Dependence (Chair: Martin Sulzmann)
The Swiss Coercion. Stefan Monnier. Implementing Reliable Linux Device Drivers in ATS. Rui Shi. Pattern matching coverage checking with dependent types using set approximations. Nicolas Oury. |
15:30-16:00 | coffee |
16:00-17:15 |
Session III: Equality, Panel (Chair: Aaron Stump) Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra. Panel discussion |