CPP 2016 - 5th ACM SIGPLAN Conference on Certified Programs and Proofs

We welcome submissions in research areas related to formal certification of programs and proofs. The following is a suggested list of topics of interest 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