default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID14th CPP 2025: Denver, CO, USA
- 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 - Emily Riehl:
Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk). 1 - Chung-Kil Hur:
CRIS: The Power of Imagination in Specification and Verification (Invited Talk). 2 - José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh:
Leakage-Free Probabilistic Jasmin Programs. 3-16 - Mircea Sebe, Maribel Fernández, James Cheney:
Nominal Matching Logic with Fixpoints. 17-33 - Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide:
Intrinsically Correct Sorting in Cubical Agda. 34-49 - Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen:
Certifying Rings of Integers in Number Fields. 50-66 - Tetsuya Sato, Yasuhiko Minamide:
Formalization of Differential Privacy in Isabelle/HOL. 67-82 - Simon Friis Vindum, Aïna Linn Georges, Lars Birkedal:
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. 83-97 - Jannis Limperg:
Tactic Script Optimisation for Aesop. 98-111 - 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 - Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters:
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. 127-139 - Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet:
Formally Verified Hardening of C Programs against Hardware Fault Injection. 140-155 - Christina Kirk, Aart Middeldorp:
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. 156-170 - Asta Halkjær From:
An Isabelle/HOL Framework for Synthetic Completeness Proofs. 171-186 - Louis Cheung, Alistair Moffat, Christine Rizkallah:
Formalized Burrows-Wheeler Transform. 187-197 - Agnishom Chattopadhyay, Wu Angela Li, Konstantinos Mamouras:
Verified and Efficient Matching of Regular Expressions with Lookaround. 198-213 - Florent Hivert:
Machine Checked Proofs and Programs in Algebraic Combinatorics. 214-230 - Akihiro Omori, Yasuhiko Minamide:
Further Tackling Post Correspondence Problem and Proof Generation. 231-242 - Katharina Heidler, Dominique Unruh:
Formalizing the One-Way to Hiding Theorem. 243-256 - Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka:
Split Decisions: Explicit Contexts for Substructural Languages. 257-271 - Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada:
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. 272-282 - 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.
last updated on 2025-12-12 23:03 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
