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

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

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)

Publisher's Version

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

Publisher's Version Info

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

Publisher's Version Info

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

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

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

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

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)

Publisher's Version Info

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 Info

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

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

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)

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)

Publisher's Version Info

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

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 Info

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

Publisher's Version

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

Publisher's Version

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

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

proc time: 4.28