From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p868FRxt014743 for ; Tue, 6 Sep 2011 10:15:27 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnIBAOvVZU7RVaE2kGdsb2JhbABCDqgLCBQBAQEBCQkNBxQEIoFfAgkjARsMAw8DEhBaAwERAQUBIxsZh1WbFwqMPYJWhHETKIhtAgMGhmQEi3KHPIxmPIMzOg X-IronPort-AV: E=Sophos;i="4.68,337,1312149600"; d="scan'208";a="107846478" Received: from mail-fx0-f54.google.com ([209.85.161.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 06 Sep 2011 10:15:21 +0200 Received: by fxe4 with SMTP id 4so7477088fxe.27 for ; Tue, 06 Sep 2011 01:15:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type :content-transfer-encoding; bh=Qn/nB+7zRniB3FYFiR5m/eZ4Onr8PNEhiHthEqqvZgE=; b=wmXnC7Nc02D0bzUIpyuOFuPBzShHS1RY4R0OABvU2SeO4fTxebjjcrbatCPipOSE8H ERdL9+H+bYFWCneJoyba8/77CcOcZ9pfAXKgwsUq7YSMio+rev+SbRvvB/3+DrALpU0F fOMfM6uWRhuOoBzpPBRRuYHtAMxqD+Q0xQY4Q= MIME-Version: 1.0 Received: by 10.223.50.143 with SMTP id z15mr2718430faf.73.1315296920575; Tue, 06 Sep 2011 01:15:20 -0700 (PDT) Received: by 10.152.22.4 with HTTP; Tue, 6 Sep 2011 01:15:20 -0700 (PDT) Date: Tue, 6 Sep 2011 10:15:20 +0200 Message-ID: From: PLPV 2012 To: finite-model-theory@lists.rwth-aachen.de, logic-list@helsinki.fi, spin_list@research.bell-labs.com, theorem-provers@ai.mit.edu, calculemus-ig@ags.uni-sb.de, concurrency@cwi.nl, formal-methods@cs.uidaho.edu, hol-info@lists.sourceforge.net, als+lics-request@inf.ed.ac.uk, metaprl@metaprl.org, pvs@csl.sri.com, acl2@cs.utexas.edu, agda@lists.chalmers.se, isabelle-users@cl.cam.ac.uk, caml-list@inria.fr, clean-list@science.ru.nl, erlang-questions@erlang.org, fp-nl@cs.uu.nl, haskell@haskell.org, plt-scheme@list.cs.brown.edu, prog-lang@diku.dk, seworld@sigsoft.org, sml-list@cs.cmu.edu Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p868FRxt014743 X-Validation-by: plpv2012@gmail.com Subject: [Caml-list] CFP: Programming Languages meets Program Verification (PLPV 2012) PLPV 2012 The Sixth ACM SIGPLAN Workshop Programming Languages meets Program Verification --- call for papers --- 24th January, 2012 Philadelphia, USA (Affiliated with POPL 2012) http://research.microsoft.com/en-us/um/people/nswamy/plpv12 -------------------------------------------------------------------------------- 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 or extended static checking systems which incorporate contracts with either static or dynamic contract checking. 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 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, 2011 Notification: 8th November, 2011 Final Version: 15th November, 2011 Workshop: 24th January, 2012 -------------------------------------------------------------------------------- Submissions We seek submissions of up to 12 pages related to the above topics---shorter submissions are also welcome. Submissions may describe new work, propose new challenge problems for language-based verification techniques, or present a known idea in an elegant way (i.e., a pearl). Submissions should be prepared with SIGPLAN two-column conference format (http://www.sigplan.org/authorInformation.htm). Submitted papers must adhere to the SIGPLAN republication policy (http://www.sigplan.org/republicationpolicy.htm). Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. To submit a paper, access the submission site at http://www.easychair.org/conferences/?conf=plpv2012. -------------------------------------------------------------------------------- Publication Accepted papers will be published by the ACM and will appear in the ACM Digital library. -------------------------------------------------------------------------------- Program Committee Amal Ahmed Indiana University Lennart Augustsson Standard Chartered Koen Claessen Chalmers (co-chair) Martin Giese University of Oslo Daniel Licata Carnegie Mellon University Peter Müller ETH Zurich Aleksandar Nanevski IMDEA Matthieu Sozeau INRIA Nikhil Swamy Microsoft Research (co-chair) David Walker Princeton University Dana Xu INRIA -------------------------------------------------------------------------------- Previous PLPVs: http://plpv.org