Author Information
Accepted Papers
Registration & Local Information
Mumbai, India, January 13 - 14, 2015
The CPP Manifesto
Past CPP
Certified Programs and Proofs (CPP 2015)
The 4th ACM-SIGPLAN Conference on
Call for Papers

Call for papers

The 4th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2015)

Mumbai, India, 13 - 14 January 2015

Co-located with POPL 2015

Website: http://cpp2015.inria.fr

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.

CPP 2015 is the fourth in the CPP conference series and will be co-located with POPL 2015 in Mumbai from 13 to 14 January 2015.

Important dates

Abstract submission: 3 October 2014, anywhere on Earth (11:59 pm, UTC-12)
Full paper submission: 10 October 2014, anywhere on Earth (11:59 pm, UTC-12)
Notification: 29 November 2014
Camera-ready deadline: 15 December 2014
Conference dates: 13 - 14 January 2015


Suggested, but not exclusive, specific topics of interest for submissions include:

Submission instructions

Submitted papers should not exceed 12 pages in the ACM SIGPLAN Proceedings format. Shorter papers are welcome and will be given equal consideration. The proceedings of the conference will be published by the ACM. Templates for ACM SIGPLAN format can be found on the ACM SIGPLAN website: http://www.sigplan.org/Resources/Author.

Papers should be submitted in PDF format, through the EasyChair submission page: https://www.easychair.org/conferences/?conf=cpp2015.

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.