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)

Publisher's Version Article: poplws19cppmain-id100-p doi:10.1145/3293880.3294087

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

Publisher's Version Article: poplws19cppmain-id101-p doi:10.1145/3293880.3294088

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)

Publisher's Version Article: poplws19cppmain-id4-p doi:10.1145/3293880.3294089

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

Publisher's Version Article: poplws19cppmain-id5-p doi:10.1145/3293880.3294090

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

Publisher's Version Article: poplws19cppmain-id38-p doi:10.1145/3293880.3294091

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

Publisher's Version Article: poplws19cppmain-id31-p doi:10.1145/3293880.3294092

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)

Publisher's Version Article: poplws19cppmain-id10-p doi:10.1145/3293880.3294093

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)

Publisher's Version Article: poplws19cppmain-id24-p doi:10.1145/3293880.3294094

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

Publisher's Version Article: poplws19cppmain-id30-p doi:10.1145/3293880.3294095

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)

Publisher's Version Article: poplws19cppmain-id27-p doi:10.1145/3293880.3294096

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

Publisher's Version Article: poplws19cppmain-id43-p doi:10.1145/3293880.3294097

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)

Publisher's Version Article: poplws19cppmain-id18-p doi:10.1145/3293880.3294098

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

Publisher's Version Article: poplws19cppmain-id33-p doi:10.1145/3293880.3294099

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

Publisher's Version Article: poplws19cppmain-id7-p doi:10.1145/3293880.3294100

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

Publisher's Version Article: poplws19cppmain-id44-p doi:10.1145/3293880.3294101

Program Verification

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

Publisher's Version Article: poplws19cppmain-id20-p doi:10.1145/3293880.3294102

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)

Publisher's Version Article: poplws19cppmain-id9-p doi:10.1145/3293880.3294103

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

Publisher's Version Article: poplws19cppmain-id40-p doi:10.1145/3293880.3294104

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

Publisher's Version Published Artifact Artifacts Available Article: poplws19cppmain-id21-p doi:10.1145/3293880.3294105

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)

Publisher's Version Article: poplws19cppmain-id22-p doi:10.1145/3293880.3294106

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)

Publisher's Version Article: poplws19cppmain-id1-p doi:10.1145/3293880.3294107

proc time: 0.05