<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div dir="ltr">## CFP for Certified Programs and Proofs (CPP 2020) ##<br>
<br>
Certified Programs and Proofs (CPP) is an international conference on<br>
practical and theoretical topics in all areas that consider<br>
certification as an essential paradigm for their work. Certification<br>
here means formal, mechanized verification of some sort, preferably<br>
with the production of independently checkable certificates.<br>
CPP spans areas of computer science, mathematics, logic, and education.<br>
<br>
CPP 2020 will be held on 20-21 January 2020 in New Orleans, Louisiana,<br>
United States and will be co-located with POPL 2020. CPP 2020 is<br>
sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG.<br>
<br>
For more information about this edition and the CPP series please visit:<br>
<a href="https://popl20.sigplan.org/home/CPP-2020" rel="noreferrer" target="_blank">https://popl20.sigplan.org/home/CPP-2020</a><br>
<br>
### News<br>
<br>
- Submission guideline news: **lightweight double-blind reviewing process**<br>
and **unrestricted appendices** that don't count against the page limit<br>
<br>
- Delighted to announce that the **invited speakers** for CPP 2020 will be:<br>
Adam Chlipala (MIT CSAIL) and Grigore Rosu (UIUC and Runtime Verification)<br>
<br>
- CPP 2020 will also host the **POPLmark 15 Year Retrospective Panel**<br>
<br>
### Important Dates<br>
<br>
- Abstract Deadline: 16 October 2019 at 23:59 AoE (UTC-12h)<br>
- Paper Submission Deadline: 21 October 2019 at 23:59 AoE (UTC-12h)<br>
- Notification: 27 November 2019<br>
- Camera Ready Deadline: 20 December 2019<br>
- Conference: 20 - 21 January 2020<br>
<br>
Deadlines expire at the end of the day, anywhere on earth. Abstract<br>
and submission deadlines are tight and there will be **no extensions**.<br>
<br>
### Topics of Interest<br>
<br>
We welcome submissions in research areas related to formal<br>
certification of programs and proofs. The following is a<br>
non-exhaustive list of topics of interests to CPP:<br>
<br>
- certified or certifying programming, compilation, linking, OS<br>
kernels, runtime systems, and security monitors;<br>
- certified mathematical libraries and mathematical theorems;<br>
- proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL,<br>
HOL-Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc)<br>
- new languages and tools for certified programming;<br>
- program analysis, program verification, and program synthesis;<br>
- program logics, type systems, and semantics for certified code;<br>
- logics for certifying concurrent and distributed systems;<br>
- mechanized metatheory, formalized programming language semantics,<br>
and logical frameworks;<br>
- higher-order logics, dependent type theory, proof theory,<br>
logical systems, separation logics, and logics for security;<br>
- verification of correctness and security properties;<br>
- formally verified blockchains and smart contracts;<br>
- certificates for decision procedures, including linear algebra,<br>
polynomial systems, SAT, SMT, and unification in algebras of interest;<br>
- certificates for semi-decision procedures, including equality,<br>
first-order logic, and higher-order unification;<br>
- certificates for program termination;<br>
- formal models of computation;<br>
- mechanized (un)decidability and computational complexity proofs;<br>
- user interfaces for proof assistants and theorem provers;<br>
- original formal proofs of known results in math or computer science;<br>
- teaching mathematics and computer science with proof assistants.<br>
<br>
### Program Committee Members<br>
<br>
- Jasmin Christian Blanchette (VU Amsterdam, Netherlands -- co-chair)<br>
- Catalin Hritcu (Inria Paris, France -- co-chair)<br>
- Nada Amin (Harvard University - USA)<br>
- Jesús María Aransay Azofra (Universidad de La Rioja - Spain)<br>
- Mauricio Ayala-Rincon (Universidade de Brasilia - Brazil)<br>
- Liron Cohen (Cornell University - USA)<br>
- Dominique Devriese (Vrije Universiteit Brussel - Belgium)<br>
- Jean-Christophe Filliâtre (CNRS - France)<br>
- Adam Grabowski (University of Bialystok - Poland)<br>
- Warren Hunt (University of Texas - USA)<br>
- Ori Lahav (Tel Aviv University - Israel)<br>
- Peter Lammich (The University of Manchester - UK)<br>
- Dominique Larchey-Wendling (Univ. de Lorraine, CNRS, LORIA - France)<br>
- Hongjin Liang (Nanjing University - China)<br>
- Assia Mahboubi (Inria and VU Amsterdam - France)<br>
- Cesar Munoz (NASA - USA)<br>
- Vivek Nigam (fortiss GmbH - Germany)<br>
- Benjamin Pierce (University of Pennsylvania - USA)<br>
- Vincent Rahli (University of Luxembourg, SnT - Luxembourg)<br>
- Christine Rizkallah (UNSW Sydney - Australia)<br>
- Ilya Sergey (Yale-NUS College and National University of Singapore)<br>
- Kathrin Stark (Saarland University - Germany)<br>
- Nikhil Swamy (Microsoft Research - USA)<br>
- Nicolas Tabareau (Inria - France)<br>
- Dmitriy Traytel (ETH Zürich - Switzerland)<br>
- Floris van Doorn (University of Pittsburgh - USA)<br>
- Akihisa Yamada (National Institute of Informatics - Japan)<br>
- Roberto Zunino (University of Trento - Italy)<br>
<br>
### Submission Guidelines<br>
<br>
Prior to the paper submission deadline, the authors should upload their<br>
**anonymized** paper in PDF format through the HotCRP system at<br>
<a href="https://cpp2020.hotcrp.com" rel="noreferrer" target="_blank">https://cpp2020.hotcrp.com</a><br>
<br>
Submissions must be written in English and provide sufficient detail<br>
to allow the program committee to assess the merits of the paper.<br>
<br>
Submitted papers must be formatted following the [ACM SIGPLAN<br>
Proceedings](<a href="http://www.sigplan.org/Resources/Author/" rel="noreferrer" target="_blank">http://www.sigplan.org/Resources/Author/</a>) format using the<br>
`acmart` style with the `sigplan` option, which provides a two-column<br>
style,<br>
using 10 point font for the main text, and a header for double blind review<br>
submission, i.e.,<br>
```<br>
\documentclass[sigplan,10pt,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}<br>
```<br>
<br>
Submitted papers should not exceed 12 pages, including tables and<br>
figures, but **excluding bibliography and clearly marked appendices**.<br>
The paper should be self contained without the appendices. Shorter<br>
papers are welcome and will be given equal consideration. Papers not<br>
conforming to the requirements concerning format and maximum length may<br>
be rejected without further consideration.<br>
<br>
CPP 2020 will employ a **lightweight double-blind reviewing process**.<br>
To facilitate this, submitted papers must adhere to two rules:<br>
<br>
1. author names and institutions must be omitted, and<br>
<br>
2. references to authors' own related work should be in the third person<br>
(e.g., not "We build on our previous work …" but rather “We build on<br>
the work of …").<br>
<br>
The purpose of this process is to help the PC and external reviewers<br>
come to an initial judgment about the paper without bias, not to make it<br>
impossible for them to discover the authors if they were to try. Nothing<br>
should be done in the name of anonymity that weakens the submission or<br>
makes the job of reviewing the paper more difficult. In particular,<br>
important background references should not be omitted or anonymized. In<br>
addition, authors are free to disseminate their ideas or draft versions<br>
of their paper as usual. For example, authors may post drafts of their<br>
papers on the web or give talks on their research ideas. POPL has<br>
answers for frequently asked questions addressing many common concerns:<br>
<a href="https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-Reviewing-FAQ" rel="noreferrer" target="_blank">https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-Reviewing-FAQ</a><br>
<br>
We encourage authors to provide any supplementary material that is<br>
required to support the claims made in the paper, such as proof scripts<br>
or experimental data. These materials must be uploaded at submission<br>
time, as an archive, not via a URL. Two forms of supplementary material<br>
may be submitted:<br>
<br>
- Anonymous supplementary material is available to the reviewers before<br>
they submit their first-draft reviews.<br>
<br>
- Non-anonymous supplementary material is available to the reviewers<br>
after they have submitted their first-draft reviews and learned the<br>
identity of the authors.<br>
<br>
Use the anonymous form whenever possible, so that the materials can be<br>
taken into account from the beginning of the reviewing process.<br>
<br>
Submitted papers must adhere to the SIGPLAN Republication Policy and the<br>
ACM Policy on Plagiarism. Concurrent submissions to other conferences,<br>
journals, workshops with proceedings, or similar forums of publication<br>
are not allowed. The PC chairs should be informed of closely related<br>
work submitted to a conference or journal in advance of submission.<br>
<br>
One author of each accepted paper is expected to present it at the<br>
conference.<br>
<br>
### Publication, copyright, and open access<br>
<br>
The CPP proceedings will be published by the ACM, and authors of accepted<br>
papers will be required to choose one of the following publication options:<br>
<br>
1. Author retains copyright of the work and grants ACM<br>
**a non-exclusive permission-to-publish license**<br>
and, optionally, licenses the work under a Creative Commons license;<br>
<br>
2. Author retains copyright of the work and grants ACM<br>
**an exclusive permission-to-publish license**;<br>
<br>
3. Author **transfers copyright** of the work to ACM.<br>
<br>
For authors who can afford it, we recommend option 1, which will make<br>
the paper **Gold Open Access**, and also encourage such authors to<br>
license their work under the CC-BY license. ACM will charge you an<br>
article processing fee for this option (currently, US$700), which you<br>
have to pay directly with the ACM.<br>
<br>
For everyone else, we recommend option 2, which is free and allows you<br>
to achieve **Green Open Access**, by uploading a pre-print of your paper<br>
to a repository that guarantees permanent archival such as arXiv or<br>
HAL. This is anyway a good idea for **timely dissemination** even if you<br>
chose option 1. Ensuring timely dissemination is particularly important<br>
for this edition, since, because of the very tight schedule, the<br>
official proceedings might not be available in time for CPP.<br>
<br>
The official CPP 2020 proceedings will also be available via SIGPLAN<br>
OpenTOC.<br>
<br>
For ACM's take on this, see their Copyright Policy and Author Rights.<br>
<br>
### Contact<br>
<br>
For any questions please contact the two PC chairs:<br>
Catalin Hritcu <<a href="mailto:catalin.hritcu@gmail.com" target="_blank">catalin.hritcu@gmail.com</a>>,<br>
Jasmin Christian Blanchette <<a href="mailto:j.c.blanchette@vu.nl" target="_blank">j.c.blanchette@vu.nl</a>></div>
</body>
</html>