From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 9EA80BCBF for ; Tue, 8 Dec 2009 09:45:32 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsUCAA71HEuBrw8EmWdsb2JhbACEKJRMgl0BAQEBAQgLCgcTrnKPL4Evgi1XBIFn X-IronPort-AV: E=Sophos;i="4.47,357,1257116400"; d="scan'208";a="38172689" Received: from ext.lri.fr ([129.175.15.4]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 07 Dec 2009 21:32:48 +0100 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id 07A4CA44F5 for ; Mon, 7 Dec 2009 21:32:48 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id rf05kSoleBEW for ; Mon, 7 Dec 2009 21:32:47 +0100 (CET) Received: from [192.168.0.10] (mry91-1-82-229-156-20.fbx.proxad.net [82.229.156.20]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id B82F6A4447 for ; Mon, 7 Dec 2009 21:32:47 +0100 (CET) Message-ID: <4B1D666F.6060101@lri.fr> Date: Mon, 07 Dec 2009 21:32:47 +0100 From: =?UTF-8?B?SmVhbi1DaHJpc3RvcGhlIEZpbGxpw6J0cmU=?= User-Agent: Thunderbird 1.5.0.14ubu (X11/20090319) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Call for Participation: PLPV 2010 X-Enigmail-Version: 0.94.2.0 OpenPGP: url=http://www.lri.fr/~filliatr/mykey.asc Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; filliatre:01 lri:01 sigplan:01 popl:01 popl:01 intersection:01 language's:01 barthe:01 barthe:01 hongwei:01 modular:01 invariants:01 theorems:01 weirich:01 rustan:01 ********************************************************************* CALL FOR PARTICIPATION PLPV 2010 The Fourth ACM SIGPLAN Workshop on Programming Languages meets Program Verification 19 January 2010 Madrid, Spain To be held in conjunction with POPL 2010 http://slang.soe.ucsc.edu/plpv10/ ********************************************************************* IMPORTANT DATES Hotel reservation deadline: December 28, 2009 (Monday) VENUE PLPV'10 and all POPL'10 affiliated events will take place at the Melia Castilla Hotel, Madrid. REGISTRATION To register for PLPV'10, follow the link from the POPL 2010 page, at http://www.cse.psu.edu/popl/10/ SCOPE 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 is 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 is extended static checking systems like ESC/Java and Spec#, which incorporate pre- and postconditions along with a static verifier for these contracts. INVITED SPEAKER Gilles Barthe, Madrid Instutite for Advanced Studies PRELIMINARY PROGRAM ---------------------- Invited Talk (9:00 - 10:00) * CertiCrypt: Formal Certification of Code-Based Cryptographic Proofs Gilles Barthe, Madrid Instutite for Advanced Studies Session 1 (10:30 - 12:00) * Singleton types here, Singleton types there, Singleton types everywhere Stefan Monnier and David Haguenauer * Operating system development with ATS Matthew Danish and Hongwei Xi * Modular Reasoning about Invariants over Shared State with Interposed Data Members Stephanie Balzer and Thomas Gross Session 2 (2:00 - 3:00) * Resource Typing in Guru Aaron Stump and Evan Austin * Free Theorems for Functional Logic Programs Jan Christiansen, Daniel Seidel and Janis Voigtländer Discussion (3:00 - 3:30) * Status update and discussion of the Trellys Project Session 3 (4:00 - 5:00) * Arity-generic datatype-generic programming Stephanie Weirich and Chris Casinghino * Challenge Benchmarks for Verification of Real-time Programs Tomas Kalibera, Gary Leavens and Jan Vitek ---------------------- PROGRAM CHAIRS * Cormac Flanagan (University of California, Santa Cruz) * Jean-Christophe Filliâtre (CNRS) PROGRAM COMMITTEE * Adam Chlipala (Harvard University) * Ranjit Jhala (University of California, San Diego) * Joseph Kiniry (University College Dublin) * Rustan Leino (Microsoft Research) * Xavier Leroy (INRIA Paris-Rocquencourt) * Conor McBride (University of Strathclyde) * Andrey Rybalchenko (Max Planck Institute for Software Systems) * Tim Sheard (Portland State University) * Stephanie Weirich (University of Pennsylvania)