[Agda] CPP 2021: Call for Participation and Lightning Talks

[Andrei Popescu]

*** 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-Lightning-Talks

#### 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 at gmail.com>,
Andrei Popescu <a.popescu at sheffield.ac.uk>,
Lennart Beringer <eberinge at cs.princeton.edu>