[Agda] (CFP) Certified Programs and Proofs 2013 - First Call for Papers

[Bas Spitters]

PRELIMINARY 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, May 30, 2013
**Submission Deadline:**        Friday, June 7, 2013
**Author Notification:**        Monday, August 19, 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                   Seoul 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                Taiwan National Technical University
Lihong Zhi                   Academica Sinica
=========================   =======================================