We welcome 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.