[TYPES/announce] CFP: PLPV 2009

[Thorsten Altenkirch]

Dear Types people

please submit papers to PLPV - this year colocated with POPL.

The workshop is now in its 3rd year and is a meeting point for
researchers from both sides of the Atlantic.

Cheers,
Thorsten

			   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 Fähndrich, 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)


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.