The 8th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2019)

We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interests to CPP. This is a non-exhaustive list and should be read as a guideline rather than a requirement.

• certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors;
• program logics, type systems, and semantics for certified code;
• certified decision procedures, mathematical libraries, and mathematical theorems;
• proof assistants and proof theory;
• new languages and tools for certified programming;
• program analysis, program verification, and proof-carrying code;
• certified secure protocols and transactions;
• 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;
• logics for certifying concurrent and distributed programs;
• higher-order logics, logical systems, separation logics, and logics for security;
• teaching mathematics and computer science with proof assistants.