Email Gateway (Aug 19 2022 at 11:14): Email Gateway (Aug 19 2022 at 11:14):From: Michael Norrish <Michael.Norrish@nicta.com.au>
[
NOTE: We have delayed our abstract submission dates by a few days to
bring ourselves into line with our co-conference, APLAS.
Abstract submission: Monday, 10 June
Final submission: Friday, 14 June
Come to sunny Australia in December to escape the northern winter!
]
CALL FOR PAPERS
===============
3rd International Conference on Certified Programs and Proofs (CPP2013)
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
========================= =======================================
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC