[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Programming Languages meets Program Verification (PLPV) 2007 Affiliated with ICFP 2007 Freiburg, Germany Topic: PLPV is concerned with language-based approaches to program verification. These approaches integrate programming language semantics and verification techniques in a tighter way than is typically done in traditional verification. An example is dependently typed programming, where types provide rich specifications, and programs may contain proof terms to establish type equivalences or satisfy pre-conditions. The motivation for this approach is to reduce the burden of program verification by taking greater advantage of semantic properties (like type properties) of the program during verification. Schedule, October 5th: 09:00-10:00 Invited Talk (Chair: Hongwei Xi) Jessie: an Intermediate Language for Java and C Verification. Claude Marché. 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. 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. 16:00-15:15 Session III: Equality, Panel (Chair: Aaron Stump) Observational Equality, Now! Thorsten Altenkirch, Conor McBride and Wouter Swierstra. Panel discussion For more information: www.plpv.org