Dear all, I'd like to encourage you to submit something to "Programming Languages meet Program Verification". The PC would love to see examples of verified Haskell programs and innovative uses of Haskell's type system. Wouter Call For Papers Programming Languages meets Program Verification (PLPV) 2009 http://sneezy.cs.nott.ac.uk/darcs/plpv09 January 20, 2009 Savannah, Georgia, USA Affiliated with POPL 2009. Invited Speaker: Manuel Fahndrich, Microsoft Research Overview: The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example are dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms. Another example are extended static checking systems like Spec#, which extends C# with pre- and postconditions along with a static verifier for these contracts. Paper Topics: We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. By co-locating with POPL 2009, we seek to broaden the scope of PLPV. For example, submissions may have diverse foundations for verification (e.g., type-based, Hoare-logic-based), target diverse kinds of programming languages (e.g., functional, imperative, object-oriented), and apply to diverse kinds of program properties (e.g., data structure invariants, security properties, temporal protocols). Submissions: Submissions should fall into one of the following three categories: 1. Regular research papers (at most 12 pages in total length). Submissions in this category should describe new work on the above or related topics. Please note that the page limit is an upper limit - shorter submissions are encouraged. 2. Work-in-progress reports (at most 6 pages in total length). Submissions in this category should describe new work that is ongoing and may not be fully completed or evaluated. 3. Proposals for challenge problems (at most 6 pages in total length). Submissions in this category should describe an application area which the author believes is a useful benchmark or important domain for language-based program verification techniques. Submissions should be prepared with SIGPLAN two-column conference format. Submitted papers must adhere to the SIGPLAN republication policy. Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. Publication: Accepted papers will be published by the ACM and appear in the ACM digital library. Important Dates: * Electronic submission: October 8, 2008, 11:59 pm, Samoa time (UTC-11) * Notification: November 8, 2008 * Final version: November 17, 2008 * Workshop: January 20, 2009 Organizers: * Thorsten Altenkirch (University of Nottingham, UK) * Todd Millstein (University of California, Los Angeles, USA) Program Committee: * Andreas Abel (University of Munich, Germany) * Thorsten Altenkirch, co-chair (University of Nottingham, UK) * Jeremy Gibbons (University of Oxford, UK) * Robert Harper (Carnegie Mellon University, USA) * K. Rustan M. Leino (Microsoft Research, USA) * Todd Millstein , co-chair (University of California, Los Angeles, USA) * Ulf Norell (Chalmers University, Sweden) * Jeremy Siek (University of Colorado, Boulder, USA) * Benjamin Werner (Ecole Polytechnique, France) * Steve Zdancewic (University of Pennsylvania, USA)