- 2024
- Arthur Adjedj, Meven Lennon-Bertrand
, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet:
Martin-Löf à la Coq. CPP 2024: 230-245 - Benedikt Ahrens
, Ralph Matthes, Niels van der Weide, Kobe Wullaert:
Displayed Monoidal Categories for the Semantics of Linear Logic. CPP 2024: 260-273 - Andrew W. Appel, Ariel Kellison:
VCFloat2: Floating-Point Error Analysis in Coq. CPP 2024: 14-29 - Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten:
UTC Time, Formally Verified. CPP 2024: 2-13 - Clément Chavanon, Frédéric Besson, Tristan Ninet:
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. CPP 2024: 89-102 - Chelsea Edmonds
, Lawrence C. Paulson:
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. CPP 2024: 132-146 - Joseph Eremondi:
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. CPP 2024: 205-217 - María Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
:
A Formalization of Complete Discrete Valuation Rings and Local Fields. CPP 2024: 190-204 - Siddhartha Gadgil, Anand Rao Tadipatri:
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. CPP 2024: 177-189 - Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
:
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. CPP 2024: 30-44 - Nao Hirokawa, Dohan Kim
, Kiraku Shintani, René Thiemann:
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. CPP 2024: 147-161 - Nikolai Kudasov, Emily Riehl, Jonathan Weinberger
:
Formalizing the ∞-Categorical Yoneda Lemma. CPP 2024: 274-290 - David Monniaux:
Memory Simulations, Security and Optimization in a Verified Compiler. CPP 2024: 103-117 - Ike Mulder, Robbert Krebbers:
Unification for Subformula Linking under Quantifiers. CPP 2024: 75-88 - Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang:
Compositional Verification of Concurrent C Programs with Search Structure Templates. CPP 2024: 60-74 - Azalea Raad:
Under-Approximation for Scalable Bug Detection (Keynote). CPP 2024: 1 - Ian Shillito, Dominik Kirst:
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. CPP 2024: 218-229 - Niels van der Weide, Nima Rasekh, Benedikt Ahrens
, Paige Randall North:
Univalent Double Categories. CPP 2024: 246-259 - Lauren M. White, Laura Titolo, J. Tanner Slagel, César A. Muñoz:
A Temporal Differential Dynamic Logic Formal Embedding. CPP 2024: 162-176 - Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey:
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. CPP 2024: 45-59 - Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner:
Lean Formalization of Extended Regular Expression Matching with Lookarounds. CPP 2024: 118-131 - Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy:
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024. ACM 2024 [contents] - 2023
- Yannick Forster
, Felix Jahn, Gert Smolka:
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP 2023: 159-166 - Reynald Affeldt
, Cyril Cohen, Ayumu Saito:
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. CPP 2023: 3-16 - Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of Hirsch Conjecture. CPP 2023: 17-29 - Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy:
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. CPP 2023: 30-46 - Anne Baanen
, Alex J. Best
, Nirvana Coppola
, Sander R. Dahmen
:
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. CPP 2023: 47-62 - Sandrine Blazy:
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). CPP 2023: 1 - Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial:
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. CPP 2023: 63-77 - Anthony Bordg, Adrián Doña Mateo:
Encoding Dependently-Typed Constructions into Simple Type Theory. CPP 2023: 78-89