# CfP: Certified Programs and Proofs (CPP)

**URL:** <https://discourse.rocq-prover.org/t/cfp-certified-programs-and-proofs-cpp/2009>\
**Category:** Announcements\
**Created:** [August 14, 2023, 6:34pm UTC](https://discourse.rocq-prover.org/t/cfp-certified-programs-and-proofs-cpp/2009 "2023-08-14T18:34:00Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [August 14, 2023, 6:34pm UTC](https://discourse.rocq-prover.org/t/cfp-certified-programs-and-proofs-cpp/2009/1 "2023-08-14T18:34:00Z")

</div>

> **[CPP 2024 - POPL 2024](https://popl24.sigplan.org/home/CPP-2024#Call-for-Papers)**
>
> 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 for their work. CPP spans areas of computer science,...

Abstract Submission Deadline: 12 September 2023 at 23:59 AoE (UTC-12h)  
Paper Submission Deadline: 19 September 2023 at 23:59 AoE (UTC-12h)

CPP welcomes submissions in research areas related to formal  
certification of programs and proofs. The following is a  
non-exhaustive list of topics of interest to CPP:  
\* certified or certifying programming, compilation, linking, OS  
kernels, runtime systems, security monitors, and hardware;  
\* certified mathematical libraries and mathematical theorems;  
\* proof assistants (e.g, ACL2, Agda, Coq, Dafny, F\*, HOL4, HOL Light,  
Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc);  
\* new languages and tools for certified programming;  
\* program analysis, program verification, and program synthesis;  
\* program logics, type systems, and semantics for certified code;  
\* logics for certifying concurrent and distributed systems;  
\* mechanized metatheory, formalized programming language semantics,  
and logical frameworks;  
\* higher-order logics, dependent type theory, proof theory, logical  
systems, separation logics, and logics for security;  
\* verification of correctness and security properties;  
\* formally verified blockchains and smart contracts;  
\* 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;  
\* formal models of computation;  
\* mechanized (un)decidability and computational complexity proofs;  
\* formally certified methods for induction and coinduction;  
\* integration of interactive and automated provers;  
\* logical foundations of proof assistants;  
\* applications of AI and machine learning to formal certification;  
\* user interfaces for proof assistants and theorem provers;  
\* teaching mathematics and computer science with proof assistants.