default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID11th CPP 2022: Philadelphia, PA, USA
- Andrei Popescu, Steve Zdancewic:
CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. ACM 2022, ISBN 978-1-4503-9182-5 - June Andronick:
The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). 1 - Andrew W. Appel
:
Coq's vibrant ecosystem for verification engineering (invited talk). 2-11 - César Muñoz:
Structural embeddings revisited (invited talk). 12 - Louis Cheung, Liam O'Connor, Christine Rizkallah:
Overcoming restraint: composing verification of foreign functions with cogent. 13-26 - Derek Egolf, Sam Lasser, Kathleen Fisher:
Verbatim++: verified, optimized, and semantically rich lexing with derivatives. 27-39 - Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino:
Formally verified superblock scheduling. 40-54 - Guillaume Ambal, Sergueï Lenglet, Alan Schmitt:
Certified abstract machines for skeletal semantics. 55-67 - Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle:
A compositional proof framework for FRETish requirements. 68-81 - Alexandre Moine, Arthur Charguéraud, François Pottier:
Specification and verification of a transient stack. 82-99 - Simon Friis Vindum, Dan Frumin, Lars Birkedal:
Mechanized verification of a fine-grained concurrent queue from meta's folly library. 100-115 - Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli:
Applying formal verification to microkernel IPC at meta. 116-129 - Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt:
Forward build systems, formally. 130-142 - William Schultz, Ian Dardik, Stavros Tripakis:
Formal verification of a distributed dynamic reconfiguration protocol. 143-152 - Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman:
A verified algebraic representation of cairo program execution. 153-165 - Denis Firsov, Dominique Unruh:
Reflection, rewinding, and coin-toss in EasyCrypt. 166-179 - Mihails Milehins:
An extension of the framework types-to-sets for Isabelle/HOL. 180-196 - Pablo Donato, Pierre-Yves Strub, Benjamin Werner:
A drag-and-drop proof tactic. 197-209 - Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader:
CertiStr: a certified string solver. 210-224 - Michael Färber:
Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. 225-238 - Oliver Nash:
Formalising lie algebras. 239-250 - Hing-Lun Chan:
Windmills of the minds: an algorithm for fermat's two squares theorem. 251-264 - Ariel Kellison:
A machine-checked direct proof of the Steiner-lehmus theorem. 265-273 - Mark Koch, Dominik Kirst:
Undecidability, incompleteness, and completeness of second-order logic in Coq. 274-290 - Dan Frumin:
Semantic cut elimination for the logic of bunched implications, formalized in Coq. 291-306 - Benedikt Ahrens, Ralph Matthes, Anders Mörtberg:
Implementing a category-theoretic framework for typed abstract syntax. 307-323 - Patricia Johann, Enrico Ghiorzi:
(Deep) induction rules for GADTs. 324-337 - Jonathan Prieto-Cubides:
On homotopy of walks and spherical maps in homotopy type theory. 338-351
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-09 23:25 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:
