default search action

combined dblp search
author search
venue search
publication search

ask others

15th CPP 2026: Rennes, France

> Home > Conferences and Workshops > CPP

SPARQL queries

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/2026
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2026
Kathrin Stark, Yannick Zakowski, Nikhil Swamy, Nicolas Tabareau:
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2026, Rennes, France, January 12-13, 2026. ACM 2026, ISBN 979-8-4007-2341-4
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Gouezel26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Gouezel26
Sébastien Gouëzel:
Higher Order Differential Calculus in Mathlib. 1-14
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Larchey-Wendling26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Larchey-Wendling26
Dominique Larchey-Wendling:
Bar Inductive Predicates for Constructive Algebra in Rocq. 15-28
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Thies26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Thies26
Holger Thies:
Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq. 29-44
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Vermande26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Vermande26
Quentin Vermande:
Cylindrical Algebraic Decomposition in Coq/Rocq. 45-58
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ArsacHP26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ArsacHP26
Samuel Arsac, Russ Harmer, Damien Pous:
Adhesive Category Theory for Graph Rewriting in Rocq. 59-74
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Chambert-LoirF26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Chambert-LoirF26
Antoine Chambert-Loir, María Inés de Frutos-Fernández:
Formalizing Polynomial Laws and the Universal Divided Power Algebra. 75-87
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NawrockiHCXWRHA26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NawrockiHCXWRHA26
Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey:
A Certifying Proof Assistant for Synthetic Mathematics in Lean. 88-103
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TothDB26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TothDB26
Balázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette:
Adding Sorts to an Isabelle Formalization of Superposition. 104-116
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Guerdi26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Guerdi26
Massin Guerdi:
A Lambda-Superposition Tactic for Isabelle/HOL. 117-127
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CirponsHMMMS26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CirponsHMMMS26
Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith:
Certifying the Decidability of the Word Problem in Monoids at Large. 128-142
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Lechenet26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Lechenet26
Jean-Christophe Léchenet:
Mechanized Dominator Tree Certification. 143-156
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LasnierYM26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LasnierYM26
Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen:
Brack: A Verified Compiler for Scheme via CakeML. 157-170
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NezamabadiMT26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NezamabadiMT26
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan:
Verified VCG and Verified Compiler for Dafny. 171-186
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TockmanSEGC26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TockmanSEGC26
Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala:
Foundational Verification of Running-Time Bounds for Interactive Programs. 187-200
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0001FT26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0001FT26
Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai:
Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda. 201-215
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Mascarenhas0M0B26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Mascarenhas0M0B26
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. 216-230
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LiY026
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LiY026
Runming Li, Yue Yao, Robert Harper:
Mechanizing Synthetic Tait Computability in Istari. 231-247
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0001HGK26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0001HGK26
Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers:
Building Blocks for Step-Indexed Program Logics. 248-263
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Korkut26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Korkut26
Joomy Korkut:
A Rose Tree Is Blooming (Proof Pearl). 264-278
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KanL26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KanL26
Shuanglong Kan, Anthony W. Lin:
Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis. 279-293
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/TrabishI26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/TrabishI26
David Trabish, Shachar Itzhaky:
Enhancing Symbolic Execution with Machine-Checked Safety Proofs. 294-308
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HenrioJKPZ26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HenrioJKPZ26
Ludovic Henrio, Einar Broch Johnsen, Åsmund Aqissiaq Arild Kløvstad, Violet Ka I Pun, Yannick Zakowski:
Layers of Confluence for Actors. 309-324
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CamaioniHYB26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CamaioniHYB26
Martina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat:
Towards Composable Proofs of Cache Coherence Protocols. 325-338
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ElbeheirySKD026
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ElbeheirySKD026
Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg:
A Recipe for Modular Verification of Generic Tree Traversals. 339-352
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GuanP26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GuanP26
Yawen Guan, Clément Pit-Claudel:
Precise Reasoning about Container-Internal Pointers with Logical Pinning. 353-367
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MarionneauB0B26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MarionneauB0B26
Virgil Marionneau, Félix Sassus Bourda, Alejandro Aguirre, Lars Birkedal:
Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. 368-382
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GolfouseGJ26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GolfouseGJ26
Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan:
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust. 383-397

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.