CPP 2016

The 5th ACM SIGPLAN Conference on

Certified Programs and Proofs

in cooperation with ACM SIGLOG

Saint Petersburg, Florida, USA - January 18-19, 2016

Downtown St. Petersburg Florida from Marina

Colocated with POPL 2016, January 20-22

Program now posted on EasyChair, including invited talks by Leonardo de Moura and Harvey Friedman!

For registration and other such information, see the POPL site.

CPP is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates.

For more information, see the CPP manifesto.

Topics of interest:

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

Call for papers

The conference proceedings will be published in the ACM Digital Library.

Important dates

  • Abstract submission: October 7, 2015
  • Submission deadline: October 12 14, 2015 (some parts of this web site were inconsistent, so we're interpreting the deadline as the later of the two that were suggested)
  • Author notification: November 18, 2015
  • Final versions due: December 4, 2015
  • Conference: January 18-19, 2016

Contact: cpp2016@easychair.org