The 6th ACM SIGPLAN Conference on
Certified Programs and Proofs (CPP 2017)
Paris, France, January 16 - 17, 2017

Conference Program

Monday, January 16th

09:00 Invited talk
-Porting the HOL Light analysis library: Some lessons [Slides/PDF]
Larry Paulson
10:30 Algorithm and library verification
-Verifying a hash table and its iterators in higher-order separation logic
François Pottier
-A Formalization of the Berlekamp-Zassenhaus factorization algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
-Formal foundations of 3D geometry to model robot manipulators
Reynald Affeldt and Cyril Cohen
14:00 Automated proof and its formal verification
-BliStrTune: Hierarchical invention of theorem proving strategies
Jan Jakubuv and Josef Urban
-Automatic cyclic termination proofs for recursive procedures in separation logic
Reuben Rowe and James Brotherston
-Formalization of Karp-Miller tree construction on Petri nets
Mitsuharu Yamamoto, Shogo Sekine and Saki Matsumoto
16:00 Formalized Mathematics with numerical computations
-A Coq formal proof of the Lax–Milgram theorem
Sylvie Boldo, François Clement, Florian Faissole, Vincent Martin and Micaela Mayero
-A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations
Érik Martin-Dorel and Pierre Roux
-Markov processes in Isabelle/HOL
Johannes Hölzl
-Formalising real numbers in homotopy type theory
Gaetan Gilbert

Tuesday, January 17th

09:00 Invited talk
-Mechanized verification of preemptive OS kernels [Slides/PDF]
Xinyu Feng
10:30 Verified programming tools
-Verified compilation of CakeML to multiple machine-code targets
Anthony Fox, Magnus O. Myreen, Yong Kiam Tan and Ramana Kumar
-Complx: a verification framework for concurrent imperative programs
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
-Verifying dynamic race detection
William Mansky, Yuanfeng Peng, Steve Zdancewic and Joseph Devietti
14:00 Homotopy Type Theory
-The HoTT library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter Lefanu Lumsdaine, Michael Shulman, Matthieu Sozeau and Bas Spitters
-Lifting proof-relevant unification to higher dimensions
Jesper Cockx and Dominique Devriese
-The Next 700 syntactical models of type theory
Simon Boulier, Pierre-Marie Pédrot and Nicolas Tabareau
16:00 Formal verification of  programming language foundations
-Type-and-scope safe programs and their proofs
Guillaume Allais, James Chapman, Conor McBride and James McKinna
-Formally verified differential dynamic logic
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Voelp and Andre Platzer
-Equivalence of System F and λ2 in Coq based on context morphism lemmas
Jonas Kaiser, Tobias Tebbi and Gert Smolka