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.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 1: Invited talk by Harvey FriedmanCPP at Room St Petersburg II
09:00
60m
Talk
Perspectives on Formal Verfication
CPP
Harvey Friedman Ohio State University
14:00 - 15:30
Session 3: Design and Implementation of Theorem ProversCPP at Room St Petersburg II
14:00
30m
Talk
The Vampire and the FOOL
CPP
Evgenii Kotelnikov Chalmers University of Technology, Laura Kovacs Chalmers University of Technology, Giles Reger University of Manchester, Andrei Voronkov University of Manchester
14:30
30m
Talk
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Lukasz Czajka University of Innsbruck
15:00
30m
Talk
Mizar Environment for Isabelle
CPP
Cezary Kaliszyk University of Innsbruck, Karol Pąk University of Bialystok, Institute of Computer Science, Josef Urban

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

09:00 - 10:00
Session 5: Invited talk by Leonardo de MouraCPP at Room St Petersburg II
09:00
60m
Talk
Dependent Type Practice
CPP
Leonardo de Moura Microsoft Research, Redmond
10:30 - 12:00
Session 6: FoundationsCPP at Room St Petersburg II
10:30
30m
Talk
A Logic of Proofs for Differential Dynamic Logic
CPP
Nathan Fulton Carnegie Mellon University, André Platzer
11:00
30m
Talk
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Floris van Doorn Carnegie Mellon University
11:30
30m
Talk
A Nominal Exploration of Intuitionism
CPP
Vincent Rahli SnT, Mark Bickford Cornell University
14:00 - 15:30
Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. Pohjola Uppsala University, Joachim Parrow Uppsala University
14:30
30m
Talk
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington
Pre-print
15:00
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-Martin University of Ottawa, Amy Felty University of Ottawa
16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
16:00
30m
Talk
Formal Verification of Control-flow Graph Flattening
CPP
Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
16:30
30m
Talk
Axiomatic Semantics for Compiler Verification
CPP
Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University
18:00 - 21:00
CPP Reception, sponsored by the DeepSpec projectCPP at Room St Petersburg I
18:00
3h
Social Event
CPP Reception, sponsored by the DeepSpec project
CPP

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
A Logic of Proofs for Differential Dynamic Logic
CPP
A Modular, Efficient Formalisation of Real Algebraic Numbers
CPP
A Nominal Exploration of Intuitionism
CPP
A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
CPP
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Axiomatic Semantics for Compiler Verification
CPP
Bisimulation Up-to Techniques for Psi-calculi
CPP
Constructing the Propositional Truncation using Non-recursive HITs
CPP
Formal Verification of Control-flow Graph Flattening
CPP
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
CPP
Formalization of a Newton series representation of polynomials
CPP
Formalizing Jordan Normal Forms in Isabelle/HOL
CPP
Higher-order Representation Predicates in Separation Logic
CPP
Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions
CPP
Mizar Environment for Isabelle
CPP
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Pre-print
Refinement Based Verification of Imperative Data Structures
CPP
The Vampire and the FOOL
CPP