POPL 2019 Co-Located Events
POPL 2019 Co-Located Events
Powered by
Conference Publishing Consulting

8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019), January 14–15, 2019, Cascais, Portugal

CPP 2019 – Proceedings

Contents - Abstracts - Authors

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


Title Page
Welcome from the Chairs
CPP 2019 Organization

Invited Talks

Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk)
Jasmin Christian Blanchette
(Vrije Universiteit Amsterdam, Netherlands)
Article Search
A Linear Logical Framework in Hybrid (Invited Talk)
Amy P. Felty
(University of Ottawa, Canada)
Article Search

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)
Article Search
Verified Solving and Asymptotics of Linear Recurrences
Manuel Eberl
(TU Munich, Germany)
Article Search Info
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
Yannick Forster, Dominik Kirst, and Gert Smolka
(Saarland University, Germany)
Article Search 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)
Article Search
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)
Article Search

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)
Article Search
Eliminating Reflection from Type Theory
Théo Winterhalter, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)
Article Search
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)
Article Search 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)
Article Search 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)
Article Search
Certified ACKBO
Alexander Lochmann and Christian Sternagel
(University of Innsbruck, Austria)
Article Search
A Verified Prover Based on Ordered Resolution
Anders Schlichtkrull, Jasmin Christian Blanchette, and Dmitriy Traytel
(DTU, Denmark; Vrije Universiteit Amsterdam, Netherlands; ETH Zurich, Switzerland)
Article Search
Autosubst 2: Reasoning with Multi-sorted de Bruijn Terms and Vector Substitutions
Kathrin Stark, Steven Schäfer, and Jonas Kaiser
(Saarland University, Germany)
Article Search Info

Program Verification

Formally Verified Big Step Semantics out of x86-64 Binaries
Ian Roessle, Freek Verbeek, and Binoy Ravindran
(Virginia Tech, USA)
Article Search
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)
Article Search Info
Dynamic Class Initialization Semantics: A Jinja Extension
Susannah Mansky and Elsa L. Gunter
(University of Illinois at Urbana-Champaign, USA)
Article Search
A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
(Purdue University, USA)
Article Search 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)
Article Search
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)
Article Search

proc time: 2.99