### 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**

#### Mon 18 Jan Times are displayed in time zone: **Guadalajara, Mexico City, Monterrey**

**Guadalajara, Mexico City, Monterrey**

09:00 - 10:00Talk | Perspectives on Formal Verfication CPP Harvey FriedmanOhio State University |

10:30 - 11:00Talk | Higher-order Representation Predicates in Separation Logic CPP | ||

11:00 - 11:30Talk | A Unified Coq Framework for Verifying C Programs with Floating-Point Computations CPP | ||

11:30 - 12:00Talk | Refinement Based Verification of Imperative Data Structures CPP Peter LammichTechnische Universität München |

14:00 - 14:30Talk | The Vampire and the FOOL CPP Evgenii KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester | ||

14:30 - 15:00Talk | Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions CPP Lukasz CzajkaUniversity of Innsbruck | ||

15:00 - 15:30Talk | Mizar Environment for Isabelle CPP Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban |

16:00 - 16:30Talk | A Modular, Efficient Formalisation of Real Algebraic Numbers CPP | ||

16:30 - 17:00Talk | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials CPP Sophie BernardINRIA, Yves BertotINRIA, Laurence RideauINRIA, Pierre-Yves StrubIMDEA Software Institute | ||

17:00 - 17:30Talk | Formalizing Jordan Normal Forms in Isabelle/HOL CPP | ||

17:30 - 18:00Talk | Formalization of a Newton series representation of polynomials CPP |

#### Tue 19 Jan Times are displayed in time zone: **Guadalajara, Mexico City, Monterrey**

**Guadalajara, Mexico City, Monterrey**

09:00 - 10:00Talk | Dependent Type Practice CPP Leonardo De MouraMicrosoft Research, Redmond |

10:30 - 11:00Talk | A Logic of Proofs for Differential Dynamic Logic CPP | ||

11:00 - 11:30Talk | Constructing the Propositional Truncation using Non-recursive HITs CPP Floris van DoornCarnegie Mellon University | ||

11:30 - 12:00Talk | A Nominal Exploration of Intuitionism CPP |

14:00 - 15:30: Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II | |||

14:00 - 14:30Talk | Bisimulation Up-to Techniques for Psi-calculi CPP | ||

14:30 - 15:00Talk | Planning for Change in a Formal Verification of the Raft Consensus Protocol CPP Doug WoosUniversity of Washington, James R. WilcoxUniversity of Washington, Steve AntonUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Michael D. ErnstUniversity of Washington, Thomas AndersonUniversity of Washington Pre-print | ||

15:00 - 15:30Talk | A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules CPP |

16:00 - 16:30Talk | Formal Verification of Control-flow Graph Flattening CPP | ||

16:30 - 17:00Talk | Axiomatic Semantics for Compiler Verification CPP |

18:00 - 21:00Social 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.