CPP 2017 – Proceedings

Frontmatter

Keynotes

Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)
Lawrence C. Paulson
(University of Cambridge, UK)


@InProceedings{CPP17p1, author = {Lawrence C. Paulson}, title = {Porting the HOL Light Analysis Library: Some Lessons (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2017}, }

Mechanized Verification of Preemptive OS Kernels (Invited Talk)
Xinyu Feng
(University of Science and Technology of China, China)


@InProceedings{CPP17p100, author = {Xinyu Feng}, title = {Mechanized Verification of Preemptive OS Kernels (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {100-99}, doi = {}, year = {2017}, }

Algorithm and Library Verification

Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic
François Pottier
(Inria, France)


@InProceedings{CPP17p199, author = {François Pottier}, title = {Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {199-198}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p213, author = {Jose Divasón and Sebastiaan Joosten and René Thiemann and Akihisa Yamada}, title = {A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {213-212}, doi = {}, year = {2017}, }

Formal Foundations of 3D Geometry to Model Robot Manipulators
Reynald Affeldt and Cyril Cohen
(AIST, Japan; Inria, France)


@InProceedings{CPP17p227, author = {Reynald Affeldt and Cyril Cohen}, title = {Formal Foundations of 3D Geometry to Model Robot Manipulators}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {227-226}, doi = {}, year = {2017}, }

Automated Proof and Its Formal Verification

BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubův and Josef Urban
(Czech Technical University, Czech Republic)


@InProceedings{CPP17p241, author = {Jan Jakubův and Josef Urban}, title = {BliStrTune: Hierarchical Invention of Theorem Proving Strategies}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {241-240}, doi = {}, year = {2017}, }

Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
Reuben N. S. Rowe and James Brotherston
(University College London, UK)


@InProceedings{CPP17p255, author = {Reuben N. S. Rowe and James Brotherston}, title = {Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {255-254}, doi = {}, year = {2017}, }

Formalization of Karp-Miller Tree Construction on Petri Nets
Mitsuharu Yamamoto, Shogo Sekine, and Saki Matsumoto
(Chiba University, Japan; Acrovision, Japan)


@InProceedings{CPP17p269, author = {Mitsuharu Yamamoto and Shogo Sekine and Saki Matsumoto}, title = {Formalization of Karp-Miller Tree Construction on Petri Nets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {269-268}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p283, author = {Sylvie Boldo and François Clément and Florian Faissole and Vincent Martin and Micaela Mayero}, title = {A Coq Formal Proof of the Lax–Milgram Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {283-282}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p297, author = {Érik Martin-Dorel and Pierre Roux}, title = {A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {297-296}, doi = {}, year = {2017}, }

Markov Processes in Isabelle/HOL
Johannes Hölzl
(TU München, Germany)


@InProceedings{CPP17p311, author = {Johannes Hölzl}, title = {Markov Processes in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {311-310}, doi = {}, year = {2017}, }

Formalising Real Numbers in Homotopy Type Theory
Gaëtan Gilbert
(ENS Lyon, France)


@InProceedings{CPP17p325, author = {Gaëtan Gilbert}, title = {Formalising Real Numbers in Homotopy Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {325-324}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p339, author = {Anthony Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar}, title = {Verified Compilation of CakeML to Multiple Machine-Code Targets}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {339-338}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p353, author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong}, title = {Complx: A Verification Framework for Concurrent Imperative Programs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {353-352}, doi = {}, year = {2017}, }

Verifying Dynamic Race Detection
William Mansky, Yuanfeng Peng, Steve Zdancewic, and Joseph Devietti
(Princeton University, USA; University of Pennsylvania, USA)


@InProceedings{CPP17p367, author = {William Mansky and Yuanfeng Peng and Steve Zdancewic and Joseph Devietti}, title = {Verifying Dynamic Race Detection}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {367-366}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p381, author = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters}, title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {381-380}, doi = {}, year = {2017}, }

Lifting Proof-Relevant Unification to Higher Dimensions
Jesper Cockx and Dominique Devriese
(KU Leuven, Belgium)


@InProceedings{CPP17p395, author = {Jesper Cockx and Dominique Devriese}, title = {Lifting Proof-Relevant Unification to Higher Dimensions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {395-394}, doi = {}, year = {2017}, }

The Next 700 Syntactical Models of Type Theory
Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau
(Inria, France)


@InProceedings{CPP17p409, author = {Simon Boulier and Pierre-Marie Pédrot and Nicolas Tabareau}, title = {The Next 700 Syntactical Models of Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {409-408}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p423, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {423-422}, doi = {}, year = {2017}, }

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)


@InProceedings{CPP17p437, author = {Brandon Bohrer and Vincent Rahli and Ivana Vukotic and Marcus Völp and André Platzer}, title = {Formally Verified Differential Dynamic Logic}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {437-436}, doi = {}, year = {2017}, }

Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas
Jonas Kaiser, Tobias Tebbi, and Gert Smolka
(Saarland University, Germany)


@InProceedings{CPP17p451, author = {Jonas Kaiser and Tobias Tebbi and Gert Smolka}, title = {Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {451-450}, doi = {}, year = {2017}, }

proc time: 0.77