CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

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 interest 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

Please see the external CPP web site for the full details.

Mon 18 Jan

CPP-2016-main
09:00 - 10:00: CPP - Session 1: Invited talk by Harvey Friedman at Room St Petersburg II
CPP-2016-main145310400000009:00 - 10:00
Talk
Harvey FriedmanOhio State University
CPP-2016-main
10:30 - 12:00: CPP - Session 2: Verifying Imperative Programs at Room St Petersburg II
CPP-2016-main145310940000010:30 - 11:00
Talk
CPP-2016-main145311120000011:00 - 11:30
Talk
CPP-2016-main145311300000011:30 - 12:00
Talk
Peter LammichTechnische Universität München
CPP-2016-main
14:00 - 15:30: CPP - Session 3: Design and Implementation of Theorem Provers at Room St Petersburg II
CPP-2016-main145312200000014:00 - 14:30
Talk
Evgenii KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester
CPP-2016-main145312380000014:30 - 15:00
Talk
Lukasz CzajkaUniversity of Innsbruck
CPP-2016-main145312560000015:00 - 15:30
Talk
Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban
CPP-2016-main
16:00 - 18:00: CPP - Session 4: Mathematics at Room St Petersburg II
CPP-2016-main145312920000016:00 - 16:30
Talk
Wenda LiUniversity of Cambridge, Lawrence PaulsonCambridge University
CPP-2016-main145313100000016:30 - 17:00
Talk
Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute
CPP-2016-main145313280000017:00 - 17:30
Talk
René ThiemannUniversity of Innsbruck, Akihisa Yamada
CPP-2016-main145313460000017:30 - 18:00
Talk

Tue 19 Jan

CPP-2016-main
09:00 - 10:00: CPP - Session 5: Invited talk by Leonardo de Moura at Room St Petersburg II
CPP-2016-main145319040000009:00 - 10:00
Talk
Leonardo De MouraMicrosoft Research, Redmond
CPP-2016-main
10:30 - 12:00: CPP - Session 6: Foundations at Room St Petersburg II
CPP-2016-main145319580000010:30 - 11:00
Talk
Nathan FultonCarnegie Mellon University, André Platzer
CPP-2016-main145319760000011:00 - 11:30
Talk
Floris van DoornCarnegie Mellon University
CPP-2016-main145319940000011:30 - 12:00
Talk
Vincent RahliSnT, Mark BickfordCornell University
CPP-2016-main
14:00 - 15:30: CPP - Session 7: Verification for Concurrent and Distributed Systems at Room St Petersburg II
CPP-2016-main145320840000014:00 - 14:30
Talk
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
CPP-2016-main145321020000014:30 - 15:00
Talk
Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington
Pre-print
CPP-2016-main145321200000015:00 - 15:30
Talk
Michel St-MartinUniversity of Ottawa, Amy FeltyUniversity of Ottawa
CPP-2016-main
16:00 - 17:00: CPP - Session 8: Compiler Verification at Room St Petersburg II
CPP-2016-main145321560000016:00 - 16:30
Talk
Sandrine BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes
CPP-2016-main145321740000016:30 - 17:00
Talk
Steven Schäfer, Sigurd SchneiderSaarland University, Gert SmolkaSaarland University
CPP-2016-main
18:00 - 21:00: CPP - CPP Reception, sponsored by the DeepSpec project at Room St Petersburg I
CPP-2016-main145322280000018:00 - 21:00
Social Event

Call for Papers

Please see the external CPP web site for the full details, but here’s a summary of the most important points.

  • Abstracts due: October 7
  • Papers due: October 12
  • Author Notification: November 18
  • Final versions due: December 4
  • Conference: January 18-19

The paper format is compatible with the one from recent POPL and ICFP conferences.

Accepted Papers

Title
Pre-print