CPP 2019 – Proceedings

8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019)

Preface

Invited Talks

Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
Jasmin Christian Blanchette
(Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP19p1, author = {Jasmin Christian Blanchette}, title = {Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3293880.3294087}, year = {2019}, } Publisher's Version

A Linear Logical Framework in Hybrid (Invited Talk)
Amy P. Felty
(University of Ottawa, Canada)


@InProceedings{CPP19p18, author = {Amy P. Felty}, title = {A Linear Logical Framework in Hybrid (Invited Talk)}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {18-17}, doi = {10.1145/3293880.3294088}, year = {2019}, } Publisher's Version

Formalization of Mathematics and Computer Algebra

A Formal Proof of Hensel's Lemma over the p-adic Integers
Robert Y. Lewis
(Vrije Universiteit Amsterdam, Netherlands)


@InProceedings{CPP19p20, author = {Robert Y. Lewis}, title = {A Formal Proof of Hensel's Lemma over the p-adic Integers}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {20-19}, doi = {10.1145/3293880.3294089}, year = {2019}, } Publisher's Version

Verified Solving and Asymptotics of Linear Recurrences
Manuel Eberl
(TU Munich, Germany)


@InProceedings{CPP19p37, author = {Manuel Eberl}, title = {Verified Solving and Asymptotics of Linear Recurrences}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {37-36}, doi = {10.1145/3293880.3294090}, year = {2019}, } Publisher's Version

On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)


@InProceedings{CPP19p54, author = {Yannick Forster and Dominik Kirst and Gert Smolka}, title = {On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {54-53}, doi = {10.1145/3293880.3294091}, year = {2019}, } Publisher's Version

Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
Wenda Li and Lawrence C. Paulson
(University of Cambridge, UK)


@InProceedings{CPP19p71, author = {Wenda Li and Lawrence C. Paulson}, title = {Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {71-70}, doi = {10.1145/3293880.3294092}, year = {2019}, } Publisher's Version

Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL
Fabian Immler and Bohua Zhan
(Carnegie Mellon University, USA; Institute of Software at Chinese Academy of Sciences, China)


@InProceedings{CPP19p88, author = {Fabian Immler and Bohua Zhan}, title = {Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {88-87}, doi = {10.1145/3293880.3294093}, year = {2019}, } Publisher's Version

Proof Theory, Theory of Programming Languages

A Proof-Theoretic Approach to Certifying Skolemization
Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller
(Inria, France; LIX, France; École Polytechnique, France)


@InProceedings{CPP19p105, author = {Kaustuv Chaudhuri and Matteo Manighetti and Dale Miller}, title = {A Proof-Theoretic Approach to Certifying Skolemization}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {105-104}, doi = {10.1145/3293880.3294094}, year = {2019}, } Publisher's Version

Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)


@InProceedings{CPP19p122, author = {Théo Winterhalter and Matthieu Sozeau and Nicolas Tabareau}, title = {Eliminating Reflection from Type Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {122-121}, doi = {10.1145/3293880.3294095}, year = {2019}, } Publisher's Version

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster and Dominique Larchey-Wendling
(Saarland University, Germany; University of Lorraine, France; CNRS, France; LORIA, France)


@InProceedings{CPP19p139, author = {Yannick Forster and Dominique Larchey-Wendling}, title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {139-138}, doi = {10.1145/3293880.3294096}, year = {2019}, } Publisher's Version

Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark
(Saarland University, Germany)


@InProceedings{CPP19p156, author = {Yannick Forster and Steven Schäfer and Simon Spies and Kathrin Stark}, title = {Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {156-155}, doi = {10.1145/3293880.3294097}, year = {2019}, } Publisher's Version

Rewriting, Automated Reasoning

A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
(University of Innsbruck, Austria; Allgemeines Rechenzentrum Innsbruck, Austria)


@InProceedings{CPP19p173, author = {Bertram Felgenhauer and Aart Middeldorp and T. V. H. Prathamesh and Franziska Rapp}, title = {A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {173-172}, doi = {10.1145/3293880.3294098}, year = {2019}, } Publisher's Version

Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)


@InProceedings{CPP19p190, author = {Alexander Lochmann and Christian Sternagel}, title = {Certified ACKBO}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {190-189}, doi = {10.1145/3293880.3294099}, year = {2019}, } Publisher's Version

A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)


@InProceedings{CPP19p207, author = {Anders Schlichtkrull and Jasmin Christian Blanchette and Dmitriy Traytel}, title = {A Verified Prover Based on Ordered Resolution}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {207-206}, doi = {10.1145/3293880.3294100}, year = {2019}, } Publisher's Version

Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)


@InProceedings{CPP19p224, author = {Kathrin Stark and Steven Schäfer and Jonas Kaiser}, title = {Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {224-223}, doi = {10.1145/3293880.3294101}, year = {2019}, } Publisher's Version

Program Verification

Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)


@InProceedings{CPP19p241, author = {Ian Roessle and Freek Verbeek and Binoy Ravindran}, title = {Formally Verified Big Step Semantics out of x86-64 Binaries}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {241-240}, doi = {10.1145/3293880.3294102}, year = {2019}, } Publisher's Version

Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
Sandrine Blazy and Rémi Hutin
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)


@InProceedings{CPP19p258, author = {Sandrine Blazy and Rémi Hutin}, title = {Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {258-257}, doi = {10.1145/3293880.3294103}, year = {2019}, } Publisher's Version

Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)


@InProceedings{CPP19p275, author = {Susannah Mansky and Elsa L. Gunter}, title = {Dynamic Class Initialization Semantics: A Jinja Extension}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {275-274}, doi = {10.1145/3293880.3294104}, year = {2019}, } Publisher's Version

A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)


@InProceedings{CPP19p292, author = {Qianchuan Ye and Benjamin Delaware}, title = {A Verified Protocol Buffer Compiler}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {292-291}, doi = {10.1145/3293880.3294105}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available

From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic
(University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)


@InProceedings{CPP19p309, author = {Nicolas Koh and Yao Li and Yishuai Li and Li-yao Xia and Lennart Beringer and Wolf Honoré and William Mansky and Benjamin C. Pierce and Steve Zdancewic}, title = {From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {309-308}, doi = {10.1145/3293880.3294106}, year = {2019}, } Publisher's Version

A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra
Véronique Benzaken and Évelyne Contejean
(University of Paris-Sud, France; LRI, France; CNRS, France)


@InProceedings{CPP19p326, author = {Véronique Benzaken and Évelyne Contejean}, title = {A Coq Mechanised Formal Semantics for Realistic SQL Queries: Formally Reconciling SQL and Bag Relational Algebra}, booktitle = {Proc.\ CPP}, publisher = {ACM}, pages = {326-325}, doi = {10.1145/3293880.3294107}, year = {2019}, } Publisher's Version

proc time: 0.69