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.
Follow this link for more information about the CPP series.
CPP 2017 is co-located with POPL 2017, in Paris, France. Registration and accommodation information will mostly be available on that site.
Important Dates
| Abstract submission: | October 5, 2016 |
| Full paper submission: | October 12, 2016 |
| Notification: | November 16, 2016 |
| Camera-ready deadline: | November 28, 2016 |
| Conference dates: | January 16-17, 2017 |
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.
Invited Speakers
- Lawrence C. Paulson, University of Cambridge
- Xinyu Feng, University of Science and Technology of China
Program Committee
- Reynald Affeldt, AIST, Japan
- Thorsten Altenkirch, University of Nottingham, UK
- Jesús Aransay, Universidad de La Rioja, Spain
- Andrea Asperti, University of Bologna, Italy
- Clark Barrett, Stanford University, USA
- Yves Bertot, INRIA, France (co-chair)
- Nikolaj Bjorner, Microsoft Research, USA
- Ana Bove, Chalmers University of Technology & University of Gothenburg, Sweden
- Delphine Demange, IRISA / University of Rennes 1, France
- Reiner Hähnle, Technische Universität Darmstadt, Germany
- Marieke Huisman, University of Twente, Netherlands
- Cezary Kaliszyk, University of Innsbruck, Austria
- Robbert Krebbers, Aarhus University, Denmark
- Ondřej Kunčar, Technische Universität München, Germany
- Mohsen Lesani, MIT, USA
- Assia Mahboubi, INRIA, France
- Michael Norrish, Data61, Australia
- Vincent Rahli, University of Luxembourg, Luxembourg
- Tom Ridge, University of Leicester, UK
- Viktor Vafeiadis, MPI-SWS, Germany (co-chair)
- Freek Verbeek, Open University of the Netherlands, Netherlands
- Steve Zdancewic, University of Pennsylvania, USA