Email Gateway (Aug 19 2022 at 10:38): Email Gateway (Aug 19 2022 at 10:38):From: Michael Norrish <michael.norrish@nicta.com.au>
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
Program Committee
^^^^^^^^^^^^^^^^^
========================= =======================================
Derek Dreyer Max Planck Institute
William Farmer McMaster University
Jean-Christophe Filiâ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 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
========================= =======================================
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC