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-main09:00 - 10:00
Talk
Harvey FriedmanOhio State University
CPP-2016-main
14:00 - 15:30: CPP - Session 3: Design and Implementation of Theorem Provers at Room St Petersburg II
CPP-2016-main14:00 - 14:30
Talk
Evgenii KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester
CPP-2016-main14:30 - 15:00
Talk
Lukasz CzajkaUniversity of Innsbruck
CPP-2016-main15: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-main16:00 - 16:30
Talk
Wenda LiUniversity of Cambridge, Lawrence PaulsonCambridge University
CPP-2016-main16:30 - 17:00
Talk
Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute
CPP-2016-main17:00 - 17:30
Talk
René ThiemannUniversity of Innsbruck, Akihisa Yamada
CPP-2016-main17: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-main09: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-main10:30 - 11:00
Talk
Nathan FultonCarnegie Mellon University, André Platzer
CPP-2016-main11:00 - 11:30
Talk
Floris van DoornCarnegie Mellon University
CPP-2016-main11: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-main14:00 - 14:30
Talk
Johannes Å. PohjolaUppsala University, Joachim ParrowUppsala University
CPP-2016-main14: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-main15: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-main16:00 - 16:30
Talk
Sandrine BlazyIRISA / University of Rennes 1, Alix TrieuENS Rennes
CPP-2016-main16: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-main18: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