default search action

combined dblp search
author search
venue search
publication search

ask others

14th CPP 2025: Denver, CO, USA

> Home > Conferences and Workshops > CPP

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/2025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2025
Kathrin Stark, Amin Timany, Sandrine Blazy, Nicolas Tabareau:
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025. ACM 2025, ISBN 979-8-4007-1347-7
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Riehl25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Riehl25
Emily Riehl:
Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk). 1
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Hur25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Hur25
Chung-Kil Hur:
CRIS: The Power of Imagination in Specification and Verification (Invited Talk). 2
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AlmeidaF0U25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AlmeidaF0U25
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh:
Leakage-Free Probabilistic Jasmin Programs. 3-16
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SebeFC25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SebeFC25
Mircea Sebe, Maribel Fernández, James Cheney:
Nominal Matching Logic with Fixpoints. 17-33
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/AlexandruCRW25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/AlexandruCRW25
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide:
Intrinsically Correct Sorting in Cubical Agda. 34-49
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BaanenVD25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BaanenVD25
Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen:
Certifying Rings of Integers in Number Fields. 50-66
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0001M25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0001M25
Tetsuya Sato, Yasuhiko Minamide:
Formalization of Differential Privacy in Isabelle/HOL. 67-82
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/VindumGB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/VindumGB25
Simon Friis Vindum, Aïna Linn Georges, Lars Birkedal:
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. 83-97
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Limperg25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Limperg25
Jannis Limperg:
Tactic Script Optimisation for Aesop. 98-111
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ZalivaM00FSS25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ZalivaM00FSS25
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell:
A CHERI C Memory Model for Verified Temporal Safety. 112-126
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MeierJPS25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MeierJPS25
Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters:
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. 127-139
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/PesinBMP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/PesinBMP25
Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet:
Formally Verified Hardening of C Programs against Hardware Fault Injection. 140-155
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KirkM25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KirkM25
Christina Kirk, Aart Middeldorp:
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. 156-170
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/From25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/From25
Asta Halkjær From:
An Isabelle/HOL Framework for Synthetic Completeness Proofs. 171-186
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CheungMR25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CheungMR25
Louis Cheung, Alistair Moffat, Christine Rizkallah:
Formalized Burrows-Wheeler Transform. 187-197
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ChattopadhyayLM25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ChattopadhyayLM25
Agnishom Chattopadhyay, Wu Angela Li, Konstantinos Mamouras:
Verified and Efficient Matching of Regular Expressions with Lookaround. 198-213
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Hivert25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Hivert25
Florent Hivert:
Machine Checked Proofs and Programs in Algebraic Combinatorics. 214-230
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/OmoriM25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/OmoriM25
Akihiro Omori, Yasuhiko Minamide:
Further Tackling Post Correspondence Problem and Proof Generation. 231-242
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HeidlerU25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HeidlerU25
Katharina Heidler, Dominique Unruh:
Formalizing the One-Way to Hiding Theorem. 243-256
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ZackonSMP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ZackonSMP25
Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka:
Split Decisions: Explicit Contexts for Substructural Languages. 257-271
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0001ST025
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0001ST025
Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada:
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. 272-282
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ChappeHZ25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ChappeHZ25
Nicolas Chappe, Ludovic Henrio, Yannick Zakowski:
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR. 283-298

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.