CPP 2026 – Proceedings |
Contents -
Abstracts -
Authors
|
Publisher's Version
ACM SIGPLAN Distinguished Paper Award
Article: poplws26cppmain-p100-p (type: Full Paper) doi:10.1145/3779031.3779102
 Higher order differential calculus in Mathlib: Recorded video presentation of "Higher order differential calculus in Mathlib". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Article: poplws26cppmain-p104-p (type: Full Paper) doi:10.1145/3779031.3779103
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p76-p (type: Full Paper) doi:10.1145/3779031.3779097
| Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq: Recorded video presentation of "Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
 |  taylor_rocqs (doi:10.5281/zenodo.17756683): This artifact provides a Rocq/Coq formalization of a constructive Taylor-series solver for multivariate analytic ordinary differential equations, together with small demonstrations and reproducible runs. |
Publisher's Version
Article: poplws26cppmain-p83-p (type: Full Paper) doi:10.1145/3779031.3779100
| Cylindrical Algebraic Decomposition in Coq/Rocq: Recorded video presentation of "Cylindrical Algebraic Decomposition in Coq/Rocq". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p114-p (type: Full Paper) doi:10.1145/3779031.3779105
| Adhesive Category Theory for Graph Rewriting in Rocq: Recorded video presentation of "Adhesive Category Theory for Graph Rewriting in Rocq". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Artifact for Adhesive Category Theory for Graph Rewriting in Rocq (doi:10.5281/zenodo.17795228): Rocq code associated with the article. |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p157-p (type: Full Paper) doi:10.1145/3779031.3779108
| Formalizing polynomial laws and the universal divided power algebra: Recorded video presentation of "Formalizing polynomial laws and the universal divided power algebra". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Formalizing Polynomial Laws and the Universal Divided Power Algebra - Lean code (doi:10.1145/3747414): This repository contains source code for the article "Formalizing polynomial laws and the universal divided power algebra", accepted to CPP 2026. The code runs over Lean 4 (v4.26.0-rc2) and Mathlib's version e814276 (November 26, 2025). |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p14-p (type: Full Paper) doi:10.1145/3779031.3779087
| A Certifying Proof Assistant for Synthetic Mathematics in Lean: Recorded video presentation of "A Certifying Proof Assistant for Synthetic Mathematics in Lean". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Implementation of "A Certifying Proof Assistant for Synthetic Mathematics in Lean" (doi:10.5281/zenodo.17798253): Implementation of the SynthLean proof assistant described in the paper "A Certifying Proof Assistant for Synthetic Mathematics in Lean". See the included file README.md for usage instructions. |
Publisher's Version
Article: poplws26cppmain-p79-p (type: Full Paper) doi:10.1145/3779031.3779099
Publisher's Version
Article: poplws26cppmain-p40-p (type: Full Paper) doi:10.1145/3779031.3779093
| A Lambda-Superposition Tactic for Isabelle/HOL: Recorded video presentation of "A Lambda-Superposition Tactic for Isabelle/HOL". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Article: poplws26cppmain-p94-p (type: Full Paper) doi:10.1145/3779031.3779101
| Certifying the decidability of the word problem in monoids at large: Recorded video presentation of "Certifying the decidability of the word problem in monoids at large". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Published Artifact
Artifacts Available
ACM SIGPLAN Distinguished Paper Award
Article: poplws26cppmain-p135-p (type: Full Paper) doi:10.1145/3779031.3779107
| Mechanized Dominator Tree Certification: Recorded video presentation of "Mechanized Dominator Tree Certification". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Artefact for "Mechanized Dominator Tree Certification", CPP 2026. (doi:10.5281/zenodo.17795214): This archive contains three directories: - CompCertSSA: the development, i.e. CompCertSSA enhanced with a certified dominator tree construction; - CompCertSSA_benchs: an instrumented version of the development used to produce the benchmarks; - benchs: the scripts executing the benchmarks, and the raw results of the ... |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p78-p (type: Full Paper) doi:10.1145/3779031.3779098
| CPP '26 Artifact - Brack: A Verified Compiler for Scheme via CakeML (doi:10.1145/3747413): Contains the Brack compiler and its end-to-end semantic preservation proof, in HOL4. Contains instructions to build and prove. |
Publisher's Version
Article: poplws26cppmain-p36-p (type: Full Paper) doi:10.1145/3779031.3779092
| Verified VCG and Verified Compiler for Dafny: Recorded video presentation of "Verified VCG and Verified Compiler for Dafny". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Article: poplws26cppmain-p17-p (type: Full Paper) doi:10.1145/3779031.3779088
Publisher's Version
Published Artifact
Info
Artifacts Available
Article: poplws26cppmain-p30-p (type: Full Paper) doi:10.1145/3779031.3779090
| Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda: Recorded video presentation of "Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda (Artefact) (doi:10.5281/zenodo.17802827): Formalisation of type theories as natural models using quotient inductive–inductive–recursive types in Cubical Agda without univalence. |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p180-p (type: Full Paper) doi:10.1145/3779031.3779111
| Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions: Recorded video presentation of "Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Lean Formalization for article "Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions" (doi:10.5281/zenodo.17810314): This artifact contains all the files in the Lean formalization of the proof calculus described in the paper. It does not contain the proof reconstruction part. This was already integrated in lean-smt and can be found on its repository: https://github.com/ufmg-smite/lean-smt. |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p2-p (type: Full Paper) doi:10.1145/3779031.3779085
| Mechanizing Synthetic Tait Computability in Istari: Recorded video presentation of "Mechanizing Synthetic Tait Computability in Istari". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Mechanizing Synthetic Tait Computability in Istari (Artifact) (doi:10.5281/zenodo.17808361): This artifact contains Istari mechanization accompanying the paper "Mechanizing Synthetic Tait Computability in Istari". |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p59-p (type: Full Paper) doi:10.1145/3779031.3779095
| Building Blocks for Step-Indexed Program Logics: Recorded video presentation of "Building Blocks for Step-Indexed Program Logics". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Rocq mechanization of "Building Blocks for Step-Indexed Program Logics" (doi:10.5281/zenodo.17809073): This artifact contains the Rocq mechanization of the CPP 2026 paper "Building Blocks for Step-Indexed Program Logics". It contains the source code for the physical step modality, as well as several Iris projects (Iris, Perennial, Trillium, LambdaRust, RefinedRust, Actris, Aneris and LinkingActris) altered to use our ... |
Publisher's Version
Article: poplws26cppmain-p33-p (type: Full Paper) doi:10.1145/3779031.3779091
| A Rose Tree is Blooming (Proof Pearl): Recorded video presentation of "A Rose Tree is Blooming (Proof Pearl)". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Article: poplws26cppmain-p58-p (type: Full Paper) doi:10.1145/3779031.3779094
| Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis: Recorded video presentation of "Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Article: poplws26cppmain-p25-p (type: Full Paper) doi:10.1145/3779031.3779089
| Enhancing Symbolic Execution with Machine-Checked Safety Proofs: Recorded video presentation of "Enhancing Symbolic Execution with Machine-Checked Safety Proofs". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p105-p (type: Full Paper) doi:10.1145/3779031.3779104
| Layers of Confluence for Actors: Recorded video presentation of "Layers of Confluence for Actors". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Layers of Confluence (doi:10.5281/zenodo.17712651): We formalise Endrullis and Klop's modern account of De Bruijn's original proof of the weak diamond property. We use it to formally prove the confluence of a class of initial configurations in a toy calculus with actors. We show how to inhabit this class of programs with concrete example using a simple but illustrative ... |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p134-p (type: Full Paper) doi:10.1145/3779031.3779106
| Towards composable proofs of cache coherence protocols: Recorded video presentation of "Towards composable proofs of cache coherence protocols". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Compositional MSI Proof (doi:10.5281/zenodo.17805558): Lean 4 development of the compositional MSI proof described in the paper. |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p173-p (type: Full Paper) doi:10.1145/3779031.3779110
| A Recipe for Modular Verification of Generic Tree Traversals: Recorded video presentation of "A Recipe for Modular Verification of Generic Tree Traversals". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| A Recipe for Modular Verification of Generic Tree Traversals (doi:10.5281/zenodo.17799204): This is the artifact accompanying the paper "A Recipe for Modular Verification of Generic Tree Traversals". The artifact contains the RefinedC proofs for the case studies presented in this paper. These proofs are carried out using the RefinedC verifier. The artifact is available as a source code archive (recipe.zip) ... |
Publisher's Version
Published Artifact
Artifacts Available
ACM SIGPLAN Distinguished Paper Award
Article: poplws26cppmain-p72-p (type: Full Paper) doi:10.1145/3779031.3779096
| Precise Reasoning about Container-Internal Pointers with Logical Pinning: Recorded video presentation of "Precise Reasoning about Container-Internal Pointers with Logical Pinning". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Artifact: Precise Reasoning about Container-Internal Pointers with Logical Pinning (doi:10.5281/zenodo.17815704): This artifact contains the mechanized formalization accompanying the article "Precise Reasoning about Container-Internal Pointers with Logical Pinning". It provides: - The complete Rocq development of the logical pinning model; - The mechanized formalization of all case studies and examples stated in the paper, ... |
Publisher's Version
Published Artifact
Artifacts Available
Article: poplws26cppmain-p165-p (type: Full Paper) doi:10.1145/3779031.3779109
| Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic: Recorded video presentation of "Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ | |
| Artifact for Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic (doi:10.5281/zenodo.17800602): This is the artifact for the CPP26 paper "Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic". It contains the Rocq files for the formalization of the results presented in the paper. Instructions for building the project and the required dependencies are described in the ... |
Publisher's Version
Article: poplws26cppmain-p8-p (type: Full Paper) doi:10.1145/3779031.3779086
| Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust: Recorded video presentation of "Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust". Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ |
proc time: 0.12