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)
Publisher's Version Article Search
Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng
(University of Science and Technology of China, China)
Publisher's Version Article Search

Algorithm and Library Verification

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

Automated Proof and Its Formal Verification

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

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

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)
Publisher's Version Article Search 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)
Publisher's Version Article Search
Verifying Dynamic Race Detection
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti
(Princeton University, USA; University of Pennsylvania, USA)
Publisher's Version Article Search 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)
Publisher's Version Article Search Info
Lifting Proof-Relevant Unification to Higher Dimensions
Jesper Cockx and Dominique Devriese
(KU Leuven, Belgium)
Publisher's Version Article Search
The Next 700 Syntactical Models of Type Theory
Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau
(Inria, France)
Publisher's Version Article Search

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

proc time: 1.16