CPP 2022

27 papers

1. (Deep) induction rules for GADTs · Patricia Johann, Enrico Ghiorzi
2. A compositional proof framework for FRETish requirements · Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle
3. A drag-and-drop proof tactic · Pablo Donato, Pierre-Yves Strub, Benjamin Werner
4. A machine-checked direct proof of the Steiner-lehmus theorem · Ariel Kellison
5. A verified algebraic representation of cairo program execution · Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
6. An extension of the framework types-to-sets for Isabelle/HOL · Mihails Milehins
7. Applying formal verification to microkernel IPC at meta · Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli
8. CertiStr: a certified string solver · Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader
9. Certified abstract machines for skeletal semantics · Guillaume Ambal, Sergueï Lenglet, Alan Schmitt
10. Coq's vibrant ecosystem for verification engineering (invited talk) · Andrew W. Appel
11. Formal verification of a distributed dynamic reconfiguration protocol · William Schultz, Ian Dardik, Stavros Tripakis
12. Formalising lie algebras · Oliver Nash
13. Formally verified superblock scheduling · Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
14. Forward build systems, formally · Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt
15. Implementing a category-theoretic framework for typed abstract syntax · Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
16. Mechanized verification of a fine-grained concurrent queue from meta's folly library · Simon Friis Vindum, Dan Frumin, Lars Birkedal
17. On homotopy of walks and spherical maps in homotopy type theory · Jonathan Prieto-Cubides
18. Overcoming restraint: composing verification of foreign functions with cogent · Louis Cheung, Liam O'Connor, Christine Rizkallah
19. Reflection, rewinding, and coin-toss in EasyCrypt · Denis Firsov, Dominique Unruh
20. Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting · Michael Färber
21. Semantic cut elimination for the logic of bunched implications, formalized in Coq · Dan Frumin
22. Specification and verification of a transient stack · Alexandre Moine, Arthur Charguéraud, François Pottier
23. Structural embeddings revisited (invited talk) · César Muñoz
24. The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk) · June Andronick
25. Undecidability, incompleteness, and completeness of second-order logic in Coq · Mark Koch, Dominik Kirst
26. Verbatim++: verified, optimized, and semantically rich lexing with derivatives · Derek Egolf, Sam Lasser, Kathleen Fisher
27. Windmills of the minds: an algorithm for fermat's two squares theorem · Hing-Lun Chan