default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID13th CPP 2024: London, UK
- 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 - Azalea Raad:
Under-Approximation for Scalable Bug Detection (Keynote). 1 - 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. 2-13 - Andrew W. Appel, Ariel Kellison:
VCFloat2: Floating-Point Error Analysis in Coq. 14-29 - 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. 30-44 - Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey:
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. 45-59 - Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang:
Compositional Verification of Concurrent C Programs with Search Structure Templates. 60-74 - Ike Mulder, Robbert Krebbers:
Unification for Subformula Linking under Quantifiers. 75-88 - Clément Chavanon, Frédéric Besson, Tristan Ninet:
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. 89-102 - David Monniaux:
Memory Simulations, Security and Optimization in a Verified Compiler. 103-117 - Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner:
Lean Formalization of Extended Regular Expression Matching with Lookarounds. 118-131 - Chelsea Edmonds, Lawrence C. Paulson:
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. 132-146 - Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann:
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. 147-161 - Lauren M. White, Laura Titolo, J. Tanner Slagel, César A. Muñoz:
A Temporal Differential Dynamic Logic Formal Embedding. 162-176 - Siddhartha Gadgil, Anand Rao Tadipatri:
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. 177-189 - 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. 190-204 - Joseph Eremondi:
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. 205-217 - Ian Shillito, Dominik Kirst:
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. 218-229 - Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet:
Martin-Löf à la Coq. 230-245 - Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North:
Univalent Double Categories. 246-259 - Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert:
Displayed Monoidal Categories for the Semantics of Linear Logic. 260-273 - Nikolai Kudasov, Emily Riehl, Jonathan Weinberger:
Formalizing the ∞-Categorical Yoneda Lemma. 274-290
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 2026-07-10 00:43 CEST 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, funded, and maintained by:
Schloss Dagstuhl - Leibniz Center for Informatics is a member of the Leibniz Association and is funded by the federal government of Germany and the states of Germany, especially Saarland and Rhineland‑Palatinate.
