CPP 2019: The 8th ACM SIGPLAN Conference on Certified Programs and Proofs CPP 2019 will be co-located with POPL 2019 Lisbon, Portugal, January 14-15, 2019 |
Conference website | https://popl19.sigplan.org/track/CPP-2019 |
Submission link | https://easychair.org/conferences/?conf=cpp2019 |
Abstract registration deadline | October 11, 2018 |
Submission deadline | October 18, 2018 |
Certified Programs and Proofs (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.
Submission Guidelines
We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interests to CPP. This is a non-exhaustive list and should be read as a guideline rather than a requirement.
* 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.
Papers should be submitted in PDF format through the EasyChair submission page at
https://easychair.org/conferences/?conf=cpp2019
Submitted papers must be formatted following the ACM SIGPLAN Proceedings format using the acmart format with the sigplan option, using 10 point font for the main text, and a header for single blind review submission, e.g.,
\documentclass[sigplan,10pt,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
Submitted papers should not exceed 12 pages, including tables and figures, but excluding bibliography. Shorter papers are welcome and will be given equal consideration.
Submissions must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. They 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. 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.
Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Dafny, Elf, HOL, HOL-Light, Isabelle, Lean, Matita, Mizar, NQTHM, PVS, Vampire, etc. Such formal developments must be submitted together with the paper as auxiliary material, and will be taken into account during the reviewing process. Please do so by including a link to your files in the text of your paper, or by sending a zip or tar file to the PC chairs with your paper number included in the subject of your email.
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 welcome. One author of each accepted paper is
expected to present it at the conference.
Program Committee
Assia | Mahboubi | Inria | co-chair | |||||||
Aaron | Dutle | NASA | ||||||||
Magnus O. | Myreen | Chalmers University of Technology | co-chair | |||||||
Jean Everson | Martina | Universidade Federal de Santa Catarina | ||||||||
Giselle | Reis | Carnegie Mellon University | ||||||||
Johannes | Hölzl | Vrije Universiteit Amsterdam | ||||||||
Chantal | Keller | LRI, Université Paris-Sud | ||||||||
Gerwin | Klein | The University of New South Wales | ||||||||
Ana | Bove | Chalmers University of Technology | ||||||||
Mauricio | Ayala-Rincon | Universidade de Brasilia | ||||||||
Andrei | Popescu | Middlesex University London | ||||||||
Enrico | Tassi | INRIA | ||||||||
Tjark | Weber | Uppsala University | ||||||||
Chris | Hawblitzel | Microsoft | ||||||||
Anna | Slobodova | Centaur Technology | ||||||||
André | Platzer | Carnegie Mellon University | ||||||||
Toby | Murray | University of Melbourne | ||||||||
Zachary | Tatlock | University of Washington | ||||||||
Christian | Sternagel | Universtity of Innsbruck | ||||||||
Bow-Yaw | Wang | Academia Sinica | ||||||||
Daniel R. | Licata | Wesleyan University | ||||||||
Aquinas | Hobor | National University of Singapore | ||||||||
John | Harrison | Amazon Web Services |