*** Call for Participation and Lightning Talks *** *** Certified Programs and Proofs (CPP 2021) ***

#### Executive Summary

* Conference dates: 17-19 January 2021 (extended to 3 days!) * Lightning talks submission deadline: 8 January 2021 (AoE) * Lightning talks session: 18 January 2021 at 20:00 CET * Registration: https://popl21.sigplan.org/attending/Registration - Early registration deadline: 10 January 2021 (!) - Discounted registration available (see below) * Long pre-recorded talks available by: 11 January 2021 (AoE)

#### General Information

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm. CPP spans areas of computer science, mathematics, logic, and education. CPP is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. For more information please visit https://popl21.sigplan.org/home/CPP-2021

CPP 2021 will be co-located with POPL 2021 and will take place on 17-19 January 2021, as a virtual meeting, where all papers are presented online. For more information about virtual conference organization have a look here: https://popl21.sigplan.org/venue/POPL-2021-venue CPP will also have both long and short versions of presentations, just that for us the short versions are 10 minutes long (not 5).

#### Call for Lightning Talks

CPP 2021 will include a session of 5-minute talks where attendees can present work-in-progress, preliminary research results, and emerging topics. Submission of such lightning talks proposals is lightweight: all we need is a title, an abstract, and the author names, affiliations, and contact information.

- Lightning talks submission deadline: 8 January 2021 (AoE) - Lightning talks session: 18 January 2021 at 20:00 CET - Submission information coming up in the next couple of days at: https://popl21.sigplan.org/home/CPP-2021#Call-for-Participation-and-Lightnin...

#### Discounted Registration

We offer a $10 alternative registration fee for anyone for whom the normal registration fees could be an impediment to participation.

#### Industrial Supporters

Warm thanks to our generous industrial supporters: - Gold supporter: JetBrains - Silver supporters: Algorand, IOHK, and Nomadic Labs - Bronze supporters: Arm, BedRock Systems Inc, Digital Asset, Galois, Informal Systems Inc, and Zilliqa

#### Invited Talks

- Tobias Nipkow (Technische Universität München): Teaching Algorithms and Data Structures with a Proof Assistant

- Peter Sewell (University of Cambridge): Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures

#### Accepted Papers, Program, and Distinguished Paper Awards

The list of papers accepted at CPP 2021 is available at https://popl21.sigplan.org/home/CPP-2021#event-overview

A preliminary program is also available: https://popl21.sigplan.org/home/CPP-2021#program

Starting with this edition we introduced the CPP Distinguished Paper Awards, aimed at accepted submissions that stand out with respect to originality, significance, and clarity. The three Distinguished Papers selected for CPP 2021 are:

- A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) by Magnus O. Myreen

- Formalizing the Ring of Witt Vectors by Johan Commelin and Robert Y. Lewis

- Machine-Checked Semantic Session Typing by Jonas Kastberg Hinrichsen, Daniel Louwrink, Robbert Krebbers and Jesper Bengtson

#### Contact

For any questions please contact the chairs: Catalin Hritcu catalin.hritcu@gmail.com, Andrei Popescu a.popescu@sheffield.ac.uk, Lennart Beringer eberinge@cs.princeton.edu