From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 86044820A2 for ; Tue, 13 Aug 2013 10:54:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of bart.jacobs@cs.kuleuven.be) identity=pra; client-ip=134.58.40.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bart.jacobs@cs.kuleuven.be"; x-sender="bart.jacobs@cs.kuleuven.be"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of bart.jacobs@cs.kuleuven.be designates 134.58.40.3 as permitted sender) identity=mailfrom; client-ip=134.58.40.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bart.jacobs@cs.kuleuven.be"; x-sender="bart.jacobs@cs.kuleuven.be"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@hermes4.cs.kuleuven.be) identity=helo; client-ip=134.58.40.3; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bart.jacobs@cs.kuleuven.be"; x-sender="postmaster@hermes4.cs.kuleuven.be"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhQCALfzCVKGOigDnGdsb2JhbABbFoJPVsBEFg4BAQEBAQgLCQkUKIJIDwYBBTMNLBEWGAMCAQIBTAwIAQGIDAEDCLdHlFoDngyORg X-IPAS-Result: AhQCALfzCVKGOigDnGdsb2JhbABbFoJPVsBEFg4BAQEBAQgLCQkUKIJIDwYBBTMNLBEWGAMCAQIBTAwIAQGIDAEDCLdHlFoDngyORg X-IronPort-AV: E=Sophos;i="4.89,867,1367964000"; d="scan'208";a="29228819" Received: from hermes4.cs.kuleuven.be ([134.58.40.3]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Aug 2013 10:54:01 +0200 Received: from hermes4.cs.kuleuven.be. (localhost [127.0.0.1]) by hermes4.cs.kuleuven.be. with ESMTP id r7D8s1i4028450 for ; Tue, 13 Aug 2013 10:54:01 +0200 Received: (from defang@localhost) by hermes4.cs.kuleuven.be. (8.14.4/8.14.4/Submit) id r7D8qbLo028393 for ; Tue, 13 Aug 2013 10:52:37 +0200 X-Authentication-Warning: hermes4.cs.kuleuven.be.: defang set sender to using -f Received: from dr-zook.cs.kuleuven.be. (dr-zook.cs.kuleuven.be [2a02:2c40:0:a005::126]) by hermes.cs.kuleuven.be (envelope-sender ) (MIMEDefang) with ESMTP id r7D8qaFB028386; Tue, 13 Aug 2013 10:52:37 +0200 Received: from localhost (localhost [127.0.0.1]) by dr-zook.cs.kuleuven.be. (8.14.4/8.14.4/Debian-2ubuntu2) with ESMTP id r7D8qZAl030415; Tue, 13 Aug 2013 10:52:35 +0200 X-Virus-Scanned: Debian amavisd-new at dr-zook.cs.kuleuven.be Received: from dr-zook.cs.kuleuven.be. ([127.0.0.1]) by localhost (dr-zook.cs.kuleuven.be [127.0.0.1]) (amavisd-new, port 10024) with LMTP id fmsVD8alYOUN; Tue, 13 Aug 2013 10:52:24 +0200 (CEST) Received: from bos.cs.kuleuven.be. (mail3.cs.kuleuven.be [IPv6:2a02:2c40:0:a000::123]) by dr-zook.cs.kuleuven.be. (8.14.4/8.14.4/Debian-2ubuntu2) with ESMTP id r7D8qED1030395 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Tue, 13 Aug 2013 10:52:14 +0200 Received: from [192.168.0.205] (94-224-99-11.access.telenet.be [94.224.99.11]) (authenticated bits=0) by bos.cs.kuleuven.be. (A_Good_MTA/8.14.3/Debian-9.1ubuntu1) with ESMTP id r7D8qCKF010181 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Tue, 13 Aug 2013 10:52:13 +0200 Message-ID: <5209F3BC.3040700@cs.kuleuven.be> Date: Tue, 13 Aug 2013 10:52:12 +0200 From: Bart Jacobs User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:17.0) Gecko/20130307 Thunderbird/17.0.4 MIME-Version: 1.0 To: pvs@csl.sri.com, twelf-list@itu.dk, rewriting@ens-lyon.fr, caml-list@yquem.inria.fr, smlnj-dev-list@lists.sourceforge.net, MLton-user@mlton.org, jmlspecs-interest@lists.sourceforge.net, ecoop-info@ecoop.org Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm X-Scanned-By: MIMEDefang 2.71 on 127.0.1.1 X-Validation-by: bart.jacobs@cs.kuleuven.be Subject: [Caml-list] CFP: PLPV 2014, Programming Languages meets Program Verification Call for papers: PLPV 2014 Programming Languages meets Program Verification San Diego, CA, USA Co-located with POPL 2014 http://www.cse.chalmers.se/~nad/plpv-2014/ 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. One example is provided by dependently typed programming languages, which make it possible to specify and check rich specifications using the languages' type systems. Another example is provided by 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 interaction between different communities, we seek a broad scope for PLPV. In particular, submissions may have diverse foundations for verification (based on types, Hoare-logic, abstract interpretation, 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 deadline: 2013-10-09T24:00-12 (midnight at the end of October 9, 2013, UTC-12) * Author notification: November 1, 2013 * Camera-ready papers due: November 17, 2013 * Workshop: January 21, 2014 Submissions ----------- For details about how to format submissions, where to send them, etc., see http://www.cse.chalmers.se/~nad/plpv-2014/call-for-papers.html. Programme committee ------------------- * Adam Chlipala, MIT * Nils Anders Danielsson, University of Gothenburg (co-chair) * Manuel Fähndrich, Microsoft Research * Philipp Haller, Typesafe * Bart Jacobs, Katholieke Universiteit Leuven (co-chair) * Chantal Keller, Aarhus University * Neelakantan R. Krishnaswami, Max Planck Institute for Software Systems * Andres Löh, Well-Typed LLP * Magnus O. Myreen, University of Cambridge * Alexander J. Summers, ETH Zurich Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm