Abstract is missing.
- Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)Emily Riehl. 1 [doi]
- CRIS: The Power of Imagination in Specification and Verification (Invited Talk)Chung-Kil Hur. 2 [doi]
- Leakage-Free Probabilistic Jasmin ProgramsJosé Bacelar Almeida, Denis Firsov, Tiago Oliveira 0004, Dominique Unruh. 3-16 [doi]
- Nominal Matching Logic with FixpointsMircea Sebe, Maribel Fernández, James Cheney. 17-33 [doi]
- Intrinsically Correct Sorting in Cubical AgdaCass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide. 34-49 [doi]
- Certifying Rings of Integers in Number FieldsAnne Baanen, Alain Chavarri Villarello, Sander R. Dahmen. 50-66 [doi]
- Formalization of Differential Privacy in Isabelle/HOLTetsuya Sato 0001, Yasuhiko Minamide. 67-82 [doi]
- The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicSimon Friis Vindum, Aïna Linn Georges, Lars Birkedal. 83-97 [doi]
- Tactic Script Optimisation for AesopJannis Limperg. 98-111 [doi]
- A CHERI C Memory Model for Verified Temporal SafetyVadim Zaliva, Kayvan Memarian, Brian Campbell 0001, Ricardo Almeida 0003, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell. 112-126 [doi]
- CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoqWolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters. 127-139 [doi]
- Formally Verified Hardening of C Programs against Hardware Fault InjectionBasile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet. 140-155 [doi]
- Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite SystemsChristina Kirk, Aart Middeldorp. 156-170 [doi]
- An Isabelle/HOL Framework for Synthetic Completeness ProofsAsta Halkjær From. 171-186 [doi]
- Formalized Burrows-Wheeler TransformLouis Cheung, Alistair Moffat, Christine Rizkallah. 187-197 [doi]
- Verified and Efficient Matching of Regular Expressions with LookaroundAgnishom Chattopadhyay, Wu Angela Li, Konstantinos Mamouras. 198-213 [doi]
- Machine Checked Proofs and Programs in Algebraic CombinatoricsFlorent Hivert. 214-230 [doi]
- Further Tackling Post Correspondence Problem and Proof GenerationAkihiro Omori, Yasuhiko Minamide. 231-242 [doi]
- Formalizing the One-Way to Hiding TheoremKatharina Heidler, Dominique Unruh. 243-256 [doi]
- Split Decisions: Explicit Contexts for Substructural LanguagesDaniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka. 257-271 [doi]
- An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term RewritingDohan Kim 0001, Teppei Saito, René Thiemann, Akihisa Yamada 0001. 272-282 [doi]
- Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IRNicolas Chappe, Ludovic Henrio, Yannick Zakowski. 283-298 [doi]