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

10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), January 18-19, 2021, Virtual, Denmark

CPP 2021 – Preliminary Table of Contents

Contents - Abstracts - Authors

10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021)

Frontmatter

Title Page
Message from the Chairs

Papers

A Modular Isabelle Framework for Verifying Saturation Provers
Sophie Tourret and Jasmin Christian Blanchette
(MPI-INF, Germany; Vrije Universiteit Amsterdam, Netherlands)
Article Search
Developing and Certifying Datalog Optimizations in Coq/MathComp
Pierre-Léo Bégay, Pierre Crégut, and Jean-François Monin
(Orange Labs, France; VERIMAG, France)
Article Search
Machine-Checked Semantic Session Typing
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson
(IT University of Copenhagen, Denmark; University of Amsterdam, Netherlands; Radboud University Nijmegen, Netherlands; Delft University of Technology, Netherlands)
Article Search
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)
Magnus O. Myreen
(Chalmers University of Technology, Sweden)
Article Search
Lutsig: A Verified Verilog Compiler for Verified Circuit Development
Andreas Lööw
(Chalmers University of Technology, Sweden)
Article Search
A Formal Proof of PAC Learnability for Decision Stumps
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee , and Jean-Baptiste Tristan
(Boston College, USA; University of Pittsburgh, USA; IMDEA Software Institute, Spain)
Article Search
A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems
Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, and Bertram Felgenhauer
(University of Innsbruck, Austria)
Article Search
Formalizing the Ring of Witt Vectors
Johan Commelin and Robert Y. Lewis
(University of Freiburg, Germany; Vrije Universiteit Amsterdam, Netherlands)
Article Search
A Coq Formalization of Data Provenance
Véronique Benzaken, Sarah Cohen-Boulakia, Contejean Eveleyne, Chantal Keller, and Rébecca Zucchini
(University of Paris-Saclay, France; LRI, France; University of Paris-Sud, France; CNRS, France)
Article Search
On the Formalisation of Kolmogorov Complexity
Elliot Catt and Michael Norrish
(Australian National University, Australia; Data61 at CSIRO, Australia)
Article Search
Formalizing Category Theory in Agda
Jason Z. S. Hu and Jacques Carette
(McGill University, Canada; McMaster University, Canada)
Article Search
Towards Efficient and Verified Virtual Machines for Dynamic Languages
Martin Desharnais and Stefan Brunthaler
(Bundeswehr University Munich, Germany)
Article Search
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
Victor Miraldo, Harold Carr, Mark Moir, Lisandra Silva, and Guy L. Steele Jr.
(Oracle Labs, n.n.; Oracle Labs, New Zealand; University of Minho, Portugal; Oracle Labs, USA)
Article Search
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar 
(MPI-SWS, Germany; McGill University, Canada)
Article Search
Formalizing Quantifiers
Olivier Laurent
(CNRS, France; ENS Lyon, France)
Article Search
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton
(University of Pittsburgh, USA; IBM Research, USA; IHES, France)
Article Search
A Novice-Friendly Induction Tactic for Lean
Jannis Limperg
(Vrije Universiteit Amsterdam, Netherlands)
Article Search
Towards Formally Verified Compilation of Tag-Based Policy Enforcement
Chris Chhak, Andrew Tolmach, and Sean Anderson
(Portland State University, USA)
Article Search
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
Simon Friis Vindum and Lars Birkedal
(Aarhus University, Denmark)
Article Search
Reasoning about Monotonicity in Separation Logic
Amin Timany and Lars Birkedal
(Aarhus University, Denmark)
Article Search
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
Dominik Kirst and Felix Rech
(Saarland University, Germany)
Article Search
Formal Verification of the Interaction between Semi-algebraic Sets and Real Analytic Functions
J. Tanner Slagel, Lauren White, and Aaron Dutle
(NASA Langley Research Center, USA; Kansas State University, USA)
Article Search
Extracting Tested and Verified Smart Contracts in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters
(Aarhus University, Denmark)
Article Search
An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR
Max W. Haslbeck and René Thiemann
(University of Innsbruck, Austria)
Article Search

proc time: 2.04