Kyoto, Japan
December 13-15, 2012
(co-located with APLAS 2012)
The conference registration site is open. The deadline for early registration is Nov. 10, 2012.
The CPP and APLAS meetings will share two keynote speakers. We are delighted that
- Xavier Leroy, INRIA and
- Greg Morrisett, Harvard University
have accepted to speak to both meetings.
We are delighted that
- Gilles Barthe (IMDEA)
- Naoki Kobayashi (University of Tokyo)
have accepted to speak at CPP 2012.
Call For Papers: html
Abstract Submission Deadline: Friday, June 8, 2012
Paper Submission Deadline: Friday, June 15, 2012
Background:
CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics and education, that consider certification as a essential paradigm for their work.
The first CPP conference was held in Kenting, Taiwan during December 7-9, 2011. As with the first meeting, the proceedings will be published in Springer-Verlag's Lecture Notes in Computer Science series.
Suggested, but not exclusive, specific topics of interest for submissions include: 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; and "Proof Pearls" (elegant, concise, and instructive examples).