Abstract is missing.
- Teaching algorithms and data structures with a proof assistant (invited talk)Tobias Nipkow. 1-3 [doi]
- Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk)Peter Sewell. 4 [doi]
- A formal proof of PAC learnability for decision stumpsJoseph Tassarotti, Koundinya Vajjha, Anindya Banerjee 0001, Jean-Baptiste Tristan. 5-17 [doi]
- CertRL: formalizing convergence proofs for value and policy iteration in CoqKoundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton. 18-31 [doi]
- A minimalistic verified bootstrapped compiler (proof pearl)Magnus O. Myreen. 32-45 [doi]
- Lutsig: a verified Verilog compiler for verified circuit developmentAndreas Lööw. 46-60 [doi]
- Towards efficient and verified virtual machines for dynamic languagesMartin Desharnais, Stefan Brunthaler. 61-75 [doi]
- Contextual refinement of the Michael-Scott queue (proof pearl)Simon Friis Vindum, Lars Birkedal. 76-90 [doi]
- Reasoning about monotonicity in separation logicAmin Timany, Lars Birkedal. 91-104 [doi]
- Extracting smart contracts tested and verified in CoqDanil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. 105-121 [doi]
- Formal verification of authenticated, append-only skip lists in AgdaVictor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr.. 122-136 [doi]
- Towards formally verified compilation of tag-based policy enforcementC. H. R. Chhak, Andrew Tolmach, Sean Anderson. 137-151 [doi]
- A Coq formalization of data provenanceVéronique Benzaken, Sarah Cohen Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini. 152-162 [doi]
- Developing and certifying Datalog optimizations in coq/mathcompPierre-Léo Bégay, Pierre Crégut, Jean-François Monin. 163-177 [doi]
- Machine-checked semantic session typingJonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson. 178-198 [doi]
- A novice-friendly induction tactic for leanJannis Limperg. 199-211 [doi]
- Lassie: HOL4 tactics by exampleHeiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar. 212-223 [doi]
- A modular Isabelle framework for verifying saturation proversSophie Tourret, Jasmin Blanchette. 224-237 [doi]
- An Isabelle/HOL formalization of AProVE's termination method for LLVM IRMax W. Haslbeck, René Thiemann. 238-249 [doi]
- A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systemsAlexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer. 250-263 [doi]
- Formalizing the ring of Witt vectorsJohan Commelin, Robert Y. Lewis. 264-277 [doi]
- Formal verification of semi-algebraic sets and real analytic functionsJ. Tanner Slagel, Lauren White, Aaron Dutle. 278-290 [doi]
- On the formalisation of Kolmogorov complexityElliot Catt, Michael Norrish. 291-299 [doi]
- An anti-locally-nameless approach to formalizing quantifiersOlivier Laurent. 300-312 [doi]
- The generalised continuum hypothesis implies the axiom of choice in CoqDominik Kirst, Felix Rech. 313-326 [doi]
- Formalizing category theory in AgdaJason Z. S. Hu, Jacques Carette. 327-342 [doi]