The Coq mailing list

[David Aspinall <da AT inf.ed.ac.uk>]

[Dear Coq club, I hope some of you may be interested in this workshop, 
papers applying Coq to prototyping or formalising PCC frameworks would 
certainly be relevant  - David.]

---

     PCC 2008: Second International Workshop on Proof-Carrying Code

                Carnegie Mellon University, 22 June 2008
                  http://workshops.inf.ed.ac.uk/pcc08

                            CALL FOR PAPERS
                       Submissions: 25 April 2008

PCC 2008 is a LICS and CSF affiliated workshop on Proof-Carrying Code. 
Proof-carrying code is an important and distinctive approach to 
enhancing trust in programs.  It provides a practical framework for 
independent assurance of program behaviour; especially where source code 
is not available, or the code author and user are unknown to each other.

The workshop will address theoretical foundations of proof-carrying code 
as well as practical examples and work on alternative application 
domains.  Here "proof" is construed broadly, to include not just 
mathematical derivations but any formal evidence that supports the 
static analysis of programs.  That is, evidence about an intrinsic 
property of code and its behaviour that can be independently checked by 
any user, intermediary, or third party.  These manifest guarantees mean 
that PCC raises trust in the code itself, distinct from and 
complementary to any existing trust in the creator of the code, the 
process used to produce it, or its distributor.

Topics include:

    * PCC addressing properties of safety, security, and correctness
      such as: Memory safety, information flow, declassification,
      resource management, access control, protocol enforcement,
      functional correctness.
    * Examples of PCC in application domains, including but not limited
      to: Mobile code, mobile devices, operating systems, grid
      computing, peer-to-peer computing, active networks, embedded
      systems, cloud computing, databases, e-Science.
    * Probabilistically-checkable proofs, zero-knowledge proofs,
      proof-on-demand.
    * Trust and policy frameworks; supporting modular and extensible
      systems; compositionality in code and proofs.
    * Certifying compilation, proof-transforming compilation, certified
      verifiers.
    * Logics and notions of certificate specific to proof-carrying
      frameworks.

PCC 2008 follows on from the successful 2006 workshop in Seattle
http://www.cs.stevens.edu/~abc/PCC-Workshop.html

INVITED SPEAKERS

    * Thomas Jensen, IRISA Rennes / CNRS
    * Zhong Shao, Yale University

IMPORTANT DATES

    * Abstract submission: 18 April 2008
    * Paper submission:    25 April 2008
    * Author notification: 23  May 2008
    * Final versions:       7 June 2008
    * Workshop:            22 June 2008

SUBMISSIONS

Papers should be in the form of a PDF file using the ENTCS style 
(http://www.entcs.org) and must not exceed 15 pages.  Submission is via 
the EasyChair system.

  http://www.easychair.org/conferences/?conf=pcc08

All submissions will be reviewed by the programme committee.  There will 
be an informal proceedings distributed at the workshop, with final 
proceedings to appear as a volume of ENTCS.

PROGRAMME COMMITTEE

    * David Aspinall, University of Edinburgh (co-chair)
    * Gilles Barthe, INRIA Sophia-Antipolis / IMDEA Software, Madrid
    * Nick Benton, Microsoft Research Cambridge
    * Adriana Compagnoni, Stevens Institute of Technology
    * Karl Crary, Carnegie Mellon University
    * Ewen Denney, NASA Ames
    * Hans-Wolfgang Loidl, LMU Munich
    * George Necula, UC Berkeley / Rinera Networks
    * Ian Stark, University of Edinburgh (co-chair)
    * Stephanie Weirich, University of Pennsylvania

ORGANISERS

  David Aspinall and Ian Stark
  School of Informatics
  The University of Edinburgh

  Contact email: 
pcc08 AT easychair.org

AFFILIATION

LICS 2008: Twenty-Third Annual IEEE Symposium on Logic in Computer Science
http://www2.informatik.hu-berlin.de/lics/lics08/

CSF: 21st IEEE Computer Security Foundations Symposium
http://www.cylab.cmu.edu/CSF2008/

Mobius: Mobility, Ubiquity, Security Enabling proof-carrying code for 
Java on mobile devices
http://mobius.inria.fr
European integrated project IST-015905

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.