[TYPES/announce] (CFP) Certified Programs and Proofs 2013 - Second Call for Papers

[Michael Norrish]

[
  NOTE: We have delayed our submission dates by a week to bring ourselves
  into line with our co-conference, APLAS.

  Come to sunny Australia to escape the northern winter!
]


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:**          Friday, June 7, 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
=========================   =======================================

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 555 bytes
Desc: OpenPGP digital signature
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130510/ffce081d/attachment-0001.sig>