CPP 2012: Call For Papers

Kyoto, Japan
December 13-15 2012

co-located with APLAS 2012


CPP is a new 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. We invite submissions on topics that fit under this rubric.

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).

Important Dates

Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT).


Program Co-chairs

Chris Hawblitzel (Microsoft Research Redmond)
Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique)

General Chair

Jacques Garrigue (Nagoya University)

Program Committee

Organizing Committee

Jacques Garrigue and Atsushi Igarashi
Email: cpp2012oc@math.nagoya-u.ac.jp

CPP Steering Committee

Andrew Appel (Princeton University)
Nikolaj Bjørner (Microsoft Research Redmond)
Georges Gonthier (Microsoft Research Cambridge)
John Harrison (Intel Corporation)
Jean-Pierre Jouannaud (co-Chair) (INRIA and Tsinghua University)
Gerwin Klein (NICTA)
Tobias Nipkow (Technische Universität München)
Zhong Shao (co-Chair) (Yale University)

Submission Instructions

Papers should be submitted electronically online via the conference submission web page at URL:


Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag’s Lecture Notes in Computer Science series.

Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration.

The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference.

CPP 2012
The Second International Conference on Certified Programs and Proofs
Home Call For Papers Organizers Important Dates Invited Speakers Submit Paper Accepted Papers Program Local Information