CPP 2017 – Proceedings

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

Frontmatter

Keynotes

Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)
Lawrence C. Paulson
(University of Cambridge, UK)
Article: cpp17key-key1-p (type: Invited Talk Abstract) doi:

Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng
(University of Science and Technology of China, China)
Article: cpp17key-key2-p (type: Invited Talk Abstract) doi:

Algorithm and Library Verification

Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
François Pottier
(Inria, France)
Article: cpp17main-mainid7-p (type: Full Paper (12 pages + references)) doi:

A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada
(Universidad de La Rioja, Spain; University of Innsbruck, Austria)
Article: cpp17main-mainid43-p (type: Full Paper (12 pages + references)) doi:

Formal Foundations of 3D Geometry to Model Robot Manipulators
Reynald Affeldt and Cyril Cohen
(AIST, Japan; Inria, France)
Article: cpp17main-mainid39-p (type: Full Paper (12 pages + references)) doi:

Automated Proof and Its Formal Verification

BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubův and Josef Urban
(Czech Technical University, Czech Republic)
Article: cpp17main-mainid25-p (type: Full Paper (12 pages + references)) doi:

Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
Reuben N. S. Rowe and James Brotherston
(University College London, UK)
Article: cpp17main-mainid5-p (type: Full Paper (12 pages + references)) doi:

Formalization of Karp-Miller Tree Construction on Petri Nets
Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto
(Chiba University, Japan; Acrovision, Japan)
Article: cpp17main-mainid36-p (type: Full Paper (12 pages + references)) doi:

Formalized Mathematics with Numerical Computations

A Coq Formal Proof of the Lax–Milgram Theorem
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero
(Inria, France; University of Paris-Sud, France; CNRS, France; University of Paris-Saclay, France; University of Technology of Compiègne, France; University of Paris North, France)
Article: cpp17main-mainid16-p (type: Full Paper (12 pages + references)) doi:

A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
Érik Martin-Dorel and Pierre Roux
(IRIT, France; Paul Sabatier University, France; ONERA, France)
Article: cpp17main-mainid6-p (type: Full Paper (12 pages + references)) doi:

Markov Processes in Isabelle/HOL
Johannes Hölzl
(TU München, Germany)
Article: cpp17main-mainid27-p (type: Full Paper (12 pages + references)) doi:

Formalising Real Numbers in Homotopy Type Theory
Gaëtan Gilbert
(ENS Lyon, France)
Article: cpp17main-mainid29-p (type: Full Paper (12 pages + references)) doi:

Verified Programming Tools

Verified Compilation of CakeML to Multiple Machine-Code Targets
Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar
(University of Cambridge, UK; Chalmers University of Technology, Sweden; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; UNSW, Australia)
Article: cpp17main-mainid14-p (type: Full Paper (12 pages + references)) doi:

Complx: A Verification Framework for Concurrent Imperative Programs
Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, and Joseph Tuong
(Data61 at CSIRO, Australia; UNSW, Australia; University of Pennsylvania, USA)
Article: cpp17main-mainid58-p (type: Full Paper (12 pages + references)) doi:

Verifying Dynamic Race Detection
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti
(Princeton University, USA; University of Pennsylvania, USA)
Article: cpp17main-mainid31-p (type: Full Paper (12 pages + references)) doi:

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
(University of Ljubljana, Slovenia; Massachusetts Institute of Technology, USA; Stockholm University, Sweden; University of San Diego, USA; Inria, France; Aarhus University, Denmark)
Article: cpp17main-mainid37-p (type: Full Paper (12 pages + references)) doi:

Lifting Proof-Relevant Unification to Higher Dimensions
Jesper Cockx and Dominique Devriese
(KU Leuven, Belgium)
Article: cpp17main-mainid17-p (type: Full Paper (12 pages + references)) doi:

The Next 700 Syntactical Models of Type Theory
Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau
(Inria, France)
Article: cpp17main-mainid34-p (type: Full Paper (12 pages + references)) doi:

Formal Verification of Programming Language Foundations

Type-and-Scope Safe Programs and Their Proofs
Guillaume Allais, James Chapman, Conor McBride, and James McKinna
(Radboud University Nijmegen, Netherlands; University of Strathclyde, UK; University of Edinburgh, UK)
Article: cpp17main-mainid28-p (type: Full Paper (12 pages + references)) doi:

Formally Verified Differential Dynamic Logic
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer
(Carnegie Mellon University, USA; University of Luxembourg, Luxembourg)
Article: cpp17main-mainid12-p (type: Full Paper (12 pages + references)) doi:

Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas
Jonas Kaiser, Tobias Tebbi, and Gert Smolka
(Saarland University, Germany)
Article: cpp17main-mainid50-p (type: Full Paper (12 pages + references)) doi: