[TYPES/announce] Call for Participation: PLPV 2010

[Jean-Christophe Filliâtre]

*********************************************************************
                         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)