![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
11th 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
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.