[Haskell] CFP: PLPV 2009

Wouter Swierstra wss at cs.nott.ac.uk
Sat Aug 9 14:02:36 EDT 2008

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.


			   Call For Papers

      Programming Languages meets Program Verification (PLPV) 2009


			   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

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  

    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

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  
     * Notification: November 8, 2008
     * Final version: November 17, 2008
     * Workshop: January 20, 2009


     * 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)

More information about the Haskell mailing list