[Agda] PLPV 2010 Call for Papers

[Wouter Swierstra]

--------------------------------------------------------------------------
                       The Fifth ACM SIGPLAN Workshop
                                                   on
               Programming Languages meets Program Verification
---------------------------------------------------------------------------
                          http://cseweb.ucsd.edu/plpv11
---------------------------------------------------------------------------


29th January, 2011
Austin, Texas
Affiliated with POPL 2011
	
Overview
--------

The goal of PLPV is to foster and stimulate research at the intersection of
programming languages and program verification, by bringing together experts
from diverse areas like types, contracts, interactive theorem proving,
model checking and program analysis. Work in this area typically attempts to
reduce the burden of program verification by taking advantage of particular
semantic or structural properties of the programming language. Examples include
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, extended static checking systems like ESC/Java
and Spec#, which incorporate contracts and static contract verifiers.

We invite submissions on all aspects, both theoretical and practical, of the
integration of programming language and program verification technology.
To encourage cross-pollination between different communities, we seek a broad
the scope for PLPV.  In particular, submissions may have diverse foundations
for verification (Type-based, Hoare-logic-based, Abstract
Interpretation-based, etc),
target different kinds of programming languages (functional,
imperative, object-oriented, etc),
and apply to diverse kinds of program properties (data structure invariants,
security properties, temporal protocols, resource constraints, etc).

Important Dates
---------------
Submission	11th October, 2010
Notification	8th November, 2010
Final Version	15th November, 2010
Workshop	29th January, 2011

Program Committee
-----------------

Andrew Gordon 		  (Microsoft Research)
Chris Hawblitzel 	  (Microsoft Research)
Ranjit Jhala 		  (University of California, San Diego, co-chair)
Viktor Kuncak 		  (Ecole Polytechnique Fédérale de Lausanne)
John Matthews 		  (Galois Inc.)
James McKinna		  (Radboud University)
Stefan Monnier		  (Université de Montréal)
Greg Morrisett 		  (Harvard University)
Christine Paulin-Mohring  (Université Paris-Sud)
Wouter Swierstra 	  (Radboud University Nijmegen , co-chair)
Tachio Terauchi 	  (Tohoku University)


Submissions
-----------

Submissions should fall into one of the following categories:

(a) Research papers (12 pages) that describe new work on the above or
related topics.
Submissions in this category have an upper limit of 12 pages but
shorter submissions
are also encouraged.

(b) Proposals for challenge problems (6 pages) which the author
believes are useful
benchmarks or important domains for language-based program
verification techniques.
Submissions in this category should be at most 6 pages in total length.

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 will appear in the
ACM Digital library.
The authors of selected papers will be invited to submit an extended
version of their
paper to a special issue of the Journal of Formalized Reasoning
devoted to papers
from PLPV 2011.

Student Attendees
-----------------
Students with accepted papers or posters are encouraged to apply for a
SIGPLAN PAC grant
that will help to cover travel expenses to PLPV. Details on the PAC
program and the
application can be found here. PAC also offers support for companion travel.