Mumbai, India, January 13 - 14, 2015
Certified Programs and Proofs (CPP 2015)
The 4th ACM-SIGPLAN Conference on
About
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.
CPP 2015 is co-located with POPL 2015, in Mumbai, India.
News
The electronic proceedings are online.
Here is the conference program.
The list of accepted papers is available.
The invited speakers for CPP 2015 are:
- Zhong Shao (Yale), on "Clean-Slate Development of Certified OS Kernels".
- Viktor Vafeiadis (MPI SWS), on "Formal Reasoning about the C11 Weak Memory Model"
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) |
| Pre-registration deadline: | 10 October 2014 (for visa purposes) |
| Notification: | 27 November 2014 |
| Camera-ready deadline: | 9 December 2014 |
| Conference dates: | 13 - 14 January 2015 |
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. Templates for ACM SIGPLAN format can be found here. Papers should be submitted in PDF format, through the EasyChair submission page before the deadline. For more detailed instructions see the call for papers.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 interests 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.
Program Committee
| Andreas Abel, Chalmers and Gothenburg University, Sweden |
| June Andronick, NICTA and UNSW, Sydney, Australia |
| Nick Benton, Microsoft Research, Cambridge, UK |
| Lennart Beringer, Princeton University, USA |
| James Brotherston. University College London, UK |
| Kaustuv Chaudhuri, Inria, Saclay, France |
| Amy Felty, University of Ottawa, Canada |
| Chung-Kil Hur , Seoul National University, Korea |
| Naoki Kobayashi, University of Tokyo, Japan |
| Xavier Leroy (co-chair), Inria, Paris-Rocquencourt, France |
| Leonardo de Moura , Microsoft Research, Redmond, USA |
| Magnus Myreen , University of Cambridge, UK |
| Vivek Nigam, Federal University of Paraíba, Brasil |
| Tobias Nipkow, Technische Universität München. Germany |
| Christine Paulin-Mohring, Université Paris-Sud, France |
| Raja Natarajan, Tata Institute of Fundamental Research, Mumbai, India |
| Gert Smolka, Saarland University, Germany |
| Alwen Tiu (co-chair), Nanyang Technological University, Singapore |
| Stephanie Weirich , University of Pennsylvania, USA |