19:08 [CPP'22] Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives ACM SIGPLAN
20:45 [CPP'22] Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr ACM SIGPLAN
24:27 [CPP'22] Semantic cut elimination for the logic of bunched implications, formalized in Coq ACM SIGPLAN
24:14 [CPP'22] Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq ACM SIGPLAN
17:20 [CPP'22] Overcoming Restraint: Composing Verification of Foreign Functions with Cogent ACM SIGPLAN
22:09 [CPP'22] Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting ACM SIGPLAN
1:06:38 [CPP'22] The seL4 verification: the art and craft of proof and the reality of commercial s ACM SIGPLAN
