share record
persistent URL:
Derek Egolf , Sam Lasser , Kathleen Fisher : Verbatim++: verified, optimized, and semantically rich lexing with derivatives. CPP 2022 : 27-39 share record
persistent URL:
Michael Färber : Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. CPP 2022 : 225-238 share record
persistent URL:
Denis Firsov , Dominique Unruh : Reflection, rewinding, and coin-toss in EasyCrypt. CPP 2022 : 166-179 share record
persistent URL:
Dan Frumin : Semantic cut elimination for the logic of bunched implications, formalized in Coq. CPP 2022 : 291-306 share record
persistent URL:
Patricia Johann , Enrico Ghiorzi : (Deep) induction rules for GADTs. CPP 2022 : 324-337 share record
persistent URL:
Shuanglong Kan , Anthony Widjaja Lin , Philipp Rümmer , Micha Schrader : CertiStr: a certified string solver. CPP 2022 : 210-224 share record
persistent URL:
Ariel Kellison : A machine-checked direct proof of the Steiner-lehmus theorem. CPP 2022 : 265-273 share record
persistent URL:
Mark Koch , Dominik Kirst : Undecidability, incompleteness, and completeness of second-order logic in Coq. CPP 2022 : 274-290 share record
persistent URL:
Mihails Milehins : An extension of the framework types-to-sets for Isabelle/HOL. CPP 2022 : 180-196 share record
persistent URL:
Alexandre Moine , Arthur Charguéraud , François Pottier : Specification and verification of a transient stack. CPP 2022 : 82-99 share record
persistent URL:
César Muñoz : Structural embeddings revisited (invited talk). CPP 2022 : 12 share record
persistent URL:
Oliver Nash : Formalising lie algebras. CPP 2022 : 239-250 export record
dblp key:
conf/cpp/Prieto-Cubides22 share record
persistent URL:
Jonathan Prieto-Cubides : On homotopy of walks and spherical maps in homotopy type theory. CPP 2022 : 338-351 share record
persistent URL:
William Schultz , Ian Dardik , Stavros Tripakis : Formal verification of a distributed dynamic reconfiguration protocol. CPP 2022 : 143-152 share record
persistent URL:
Cyril Six , Léo Gourdin , Sylvain Boulmé , David Monniaux , Justus Fasse , Nicolas Nardino : Formally verified superblock scheduling. CPP 2022 : 40-54 share record
persistent URL:
Sarah Spall , Neil Mitchell , Sam Tobin-Hochstadt : Forward build systems, formally. CPP 2022 : 130-142 share record
persistent URL:
Simon Friis Vindum , Dan Frumin , Lars Birkedal : Mechanized verification of a fine-grained concurrent queue from meta's folly library. CPP 2022 : 100-115 share record
persistent URL:
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 [contents] 2021 share record
persistent URL:
Danil Annenkov , Mikkel Milo , Jakob Botsch Nielsen , Bas Spitters : Extracting smart contracts tested and verified in Coq. CPP 2021 : 105-121 share record
persistent URL:
Heiko Becker , Nathaniel Bos , Ivan Gavran , Eva Darulova , Rupak Majumdar : Lassie: HOL4 tactics by example. CPP 2021 : 212-223 share record
persistent URL:
Pierre-Léo Bégay , Pierre Crégut , Jean-François Monin : Developing and certifying Datalog optimizations in coq/mathcomp. CPP 2021 : 163-177 share record
persistent URL:
Véronique Benzaken , Sarah Cohen-Boulakia , Evelyne Contejean , Chantal Keller , Rébecca Zucchini : A Coq formalization of data provenance. CPP 2021 : 152-162 share record
persistent URL:
Elliot Catt , Michael Norrish : On the formalisation of Kolmogorov complexity. CPP 2021 : 291-299 share record
persistent URL:
C. H. R. Chhak , Andrew Tolmach , Sean Noble Anderson : Towards formally verified compilation of tag-based policy enforcement. CPP 2021 : 137-151 share record
persistent URL:
Johan Commelin , Robert Y. Lewis : Formalizing the ring of Witt vectors. CPP 2021 : 264-277 share record
persistent URL:
Martin Desharnais , Stefan Brunthaler : Towards efficient and verified virtual machines for dynamic languages. CPP 2021 : 61-75 share record
persistent URL:
Max W. Haslbeck , René Thiemann : An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. CPP 2021 : 238-249 share record
persistent URL:
Jonas Kastberg Hinrichsen , Daniël Louwrink , Robbert Krebbers , Jesper Bengtson : Machine-checked semantic session typing. CPP 2021 : 178-198 share record
persistent URL:
Jason Z. S. Hu , Jacques Carette : Formalizing category theory in Agda. CPP 2021 : 327-342 share record
persistent URL:
Dominik Kirst , Felix Rech : The generalised continuum hypothesis implies the axiom of choice in Coq. CPP 2021 : 313-326