default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID12th CPP 2023: Boston, MA, USA
- Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. ACM 2023 - Sandrine Blazy:
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). 1 - Cezary Kaliszyk:
Improved Assistance for Interactive Proof (Keynote). 2 - Reynald Affeldt
, Cyril Cohen, Ayumu Saito:
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. 3-16 - Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub:
A Formal Disproof of Hirsch Conjecture. 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. 30-46 - Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen:
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. 47-62 - 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. 63-77 - Anthony Bordg, Adrián Doña Mateo:
Encoding Dependently-Typed Constructions into Simple Type Theory. 78-89 - Joshua Clune:
A Formalized Reduction of Keller's Conjecture. 90-101 - Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi:
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. 102-120 - Floris van Doorn, Patrick Massot, Oliver Nash:
Formalising the h-Principle and Sphere Eversion. 121-134 - Michael Färber:
Terms for Efficient Proof Checking and Parsing. 135-147 - Hugo Férée, Sam van Gool:
Formalizing and Computing Propositional Quantifiers. 148-158 - Yannick Forster, Felix Jahn, Gert Smolka:
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). 159-166 - Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi:
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. 167-181 - Yann Herklotz, Delphine Demange, Sandrine Blazy:
Mechanised Semantics for Gated Static Single Assignment. 182-196 - Christina Kohl, Aart Middeldorp:
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. 197-210 - Katherine Kosaian, Yong Kiam Tan, André Platzer:
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. 211-224 - Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds:
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. 225-238 - Thomas Lamiaux, Axel Ljungström, Anders Mörtberg:
Computing Cohomology Rings in Cubical Agda. 239-252 - Jannis Limperg, Asta Halkjær From:
Aesop: White-Box Best-First Proof Search for Lean. 253-266 - Bhavik Mehta:
Formalising Sharkovsky's Theorem (Proof Pearl). 267-274 - Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy:
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. 275-289 - Eske Hoy Nielsen, Danil Annenkov, Bas Spitters:
Formalising Decentralised Exchanges in Coq. 290-302 - Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster:
P4Cub: A Little Language for Big Routers. 303-319 - Brae J. Webb, Ian J. Hayes, Mark Utting:
Verifying Term Graph Optimizations using Isabelle/HOL. 320-333 - Kexing Ying, Rémy Degenne:
A Formalization of Doob's Martingale Convergence Theorems in mathlib. 334-347
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:
