The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

CALL FOR PAPERS

===============

 

Third International Conference on Certified Programs and Proofs (CPP 2013)

--------------------------------------------------------------------------

 

December 2013, Australia (co-located with APLAS 2013)

 

CPP is an international forum on theoretical and practical topics in

all areas, including computer science, mathematics, and education,

that consider certification as an essential paradigm for their

work. Certification here means formal, mechanized verification of some

sort, preferably with production of independently checkable

certificates. We invite submissions on topics that fit under this

rubric.

 

The first two CPP conferences were held in Kenting, Taiwan, and Kyoto,

Japan, in December 2011 and 2012, respectively. As with the first

meetings, the proceedings will be published in Springer-Verlag’s

Lecture Notes in Computer Science series.

 

Suggested, but not exclusive, specific topics of interest for

submissions include: certified or certifying programming, compilation,

linking, OS kernels, runtime systems, and security monitors; program

logics, type systems, and semantics for certified code; certified

decision procedures, mathematical libraries, and mathematical

theorems; proof assistants and proof theory; new languages and tools

for certified programming; program analysis, program verification, and

proof-carrying code; certified secure protocols and transactions;

certificates for decision procedures, including linear algebra,

polynomial systems, SAT, SMT, and unification in algebras of interest;

certificates for semi-decision procedures, including equality,

first-order logic, and higher-order unification; certificates for

program termination; logics for certifying concurrent and distributed

programs; higher-order logics, logical systems, separation logics, and

logics for security; teaching mathematics and computer science with

proof assistants; and “Proof Pearls” (elegant, concise, and

instructive examples).

 

Important Dates:

++++++++++++++++

 

Authors are required to submit a paper title and a short abstract

before submitting the full paper. The submission should include when

necessary a URL where to find the formal development assessing the

essential aspects of the work.  All submissions will be

electronic. All deadlines are at midnight (GMT).

 

============================    ==========================

**Abstract Deadline:**          Monday, June 10, 2013

**Submission Deadline:**        Friday, June 14, 2013

**Author Notification:**        Monday, August 26, 2013

**Camera-ready Papers Due:**    Monday, September 16, 2013

============================    ==========================

 

Submission Instructions:

++++++++++++++++++++++++

 

Papers should be submitted electronically online via the conference

submission web page at URL:

 

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

 

Acceptable formats are PostScript or PDF, viewable by Ghostview or

Acrobat Reader. Submissions should not exceed 16 pages in LNCS format,

including bibliography and figures.  Submitted papers will be judged

on the basis of significance, relevance, correctness, originality, and

clarity. They should clearly identify what has been accomplished and

why it is significant. The proceedings of the symposium will be

published as a volume in Springer-Verlag’s Lecture Notes in Computer

Science series. Submission instructions including LaTeX style files

are available from the CPP 2013 website.

 

Each submission must be written in English and provide sufficient

detail to allow the program committee to assess the merits of the

paper.  It should begin with a succinct statement of the issues, a

summary of the main results, and a brief explanation of their

significance and relevance to the conference, all phrased for the

non-specialist.  Technical and formal developments directed to the

specialist should follow.  Whenever appropriate, the submission should

come along with a formal development, using whatever prover, e.g.,

Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS,

Vampire, etc. References and comparisons with related work should be

included.  *Papers not conforming to the above requirements concerning

format and length may be rejected without further consideration.*

 

The results must be unpublished and not submitted for publication

elsewhere, including the proceedings of other published conferences or

workshops.  The PC chairs should be informed of closely related work

submitted to a conference or journal in advance of

submission. Original formal proofs of known results in mathematics or

computer science are among the targets.  One author of each accepted

paper is expected to present it at the conference.

 

Organisation

++++++++++++

 

:Program Co-Chairs:

  Georges Gonthier (Microsoft Research Cambridge) &

  Michael Norrish (NICTA)

 

:General Chair:

  Peter Schachte, *University of Melbourne*

 

:Website:

  http://cpp2013.forge.nicta.com.au

 

Program Committee

^^^^^^^^^^^^^^^^^

 

=========================   =======================================

Derek Dreyer                 MPI-SWS

William Farmer               McMaster University

Jean-Christophe Filliâtre    INRIA

Cédric Fournet               Microsoft Research Cambridge

Benjamin Grégoire            INRIA

Reiner Hähnle                Technische Universität Darmstadt

Aquinas Hobor                National University of Singapore

Gyesik Lee                   Hankyong National University

Cesar Muñoz                  NASA Langley

Toby Murray                  NICTA

Gopalan Nadathur             University of Minnesota

Claudio Sacerdoti Coen       University of Bologna

Peter Sewell                 University of Cambridge

Bas Spitters                 University of Nijmegen

Gang Tan                     Lehigh University

Alwen Tiu                    Australian National University

Yih-Kuen Tsay                National Taiwan University

Lihong Zhi                   Academia Sinica

=========================   =======================================