CPP 2024

21 papers

1. A Formalization of Complete Discrete Valuation Rings and Local Fields · María Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
2. A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic · Ian Shillito, Dominik Kirst
3. A Temporal Differential Dynamic Logic Formal Embedding · Lauren M. White, Laura Titolo, J. Tanner Slagel, César A. Muñoz
4. Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs · Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
5. Compositional Verification of Concurrent C Programs with Search Structure Templates · Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang
6. Displayed Monoidal Categories for the Semantics of Linear Logic · Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
7. Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma · Chelsea Edmonds, Lawrence C. Paulson
8. Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture · Siddhartha Gadgil, Anand Rao Tadipatri
9. Formalizing the ∞-Categorical Yoneda Lemma · Nikolai Kudasov, Emily Riehl, Jonathan Weinberger
10. Lean Formalization of Extended Regular Expression Matching with Lookarounds · Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
11. Martin-Löf à la Coq · Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
12. Memory Simulations, Security and Optimization in a Verified Compiler · David Monniaux
13. PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams · Clément Chavanon, Frédéric Besson, Tristan Ninet
14. Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic · Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey
15. Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments · Joseph Eremondi
16. The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography · Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
17. UTC Time, Formally Verified · Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten
18. Under-Approximation for Scalable Bug Detection (Keynote) · Azalea Raad
19. Unification for Subformula Linking under Quantifiers · Ike Mulder, Robbert Krebbers
20. Univalent Double Categories · Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
21. VCFloat2: Floating-Point Error Analysis in Coq · Andrew W. Appel, Ariel Kellison