[TYPES/announce] Call for Participation: PLPV 2007

[Aaron Stump]

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