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

CPP 2017 – Proceedings

 Contents - Abstracts - Authors

Frontmatter

Title Page
Welcome from the Chairs
CPP 2017 Organization
CPP 2017 Sponsors

Keynotes

Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)
Lawrence C. Paulson
(University of Cambridge, UK)
Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng
(University of Science and Technology of China, China)

Algorithm and Library Verification

Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
François Pottier
(Inria, France)
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)
Formal Foundations of 3D Geometry to Model Robot Manipulators
Reynald Affeldt and Cyril Cohen
(AIST, Japan; Inria, France)

Automated Proof and Its Formal Verification

BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubův and Josef Urban
(Czech Technical University, Czech Republic)
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
Reuben N. S. Rowe and James Brotherston
(University College London, UK)
Info
Formalization of Karp-Miller Tree Construction on Petri Nets
Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto
(Chiba University, Japan; Acrovision, Japan)

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)
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)
Info
Markov Processes in Isabelle/HOL
Johannes Hölzl
(TU München, Germany)
Formalising Real Numbers in Homotopy Type Theory
Gaëtan Gilbert
(ENS Lyon, France)

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)
Info
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)
Verifying Dynamic Race Detection
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti
(Princeton University, USA; University of Pennsylvania, USA)
Info

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)
Info
Lifting Proof-Relevant Unification to Higher Dimensions
Jesper Cockx and Dominique Devriese
(KU Leuven, Belgium)
The Next 700 Syntactical Models of Type Theory
Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau
(Inria, France)

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)
Info
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)
Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas
Jonas Kaiser, Tobias Tebbi, and Gert Smolka
(Saarland University, Germany)
Info

proc time: 0.66