Abstract is missing.
- Deeper Shallow EmbeddingsJacob Prinz, G. A. Kavvos, Leonidas Lampropoulos. [doi]
- Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOLAsta Halkjær From, Frederik Krogsdal Jacobsen. [doi]
- Reflexive Tactics for Algebra, RevisitedKazuhiko Sakaguchi. [doi]
- Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)Amy P. Felty. [doi]
- Formalization of a Stochastic Approximation TheoremKoundinya Vajjha, Barry M. Trager, Avraham Shinnar, Vasily Pestun. [doi]
- Formalizing a Diophantine Representation of the Set of Prime NumbersKarol Pak, Cezary Kaliszyk. [doi]
- Dandelion: Certified Approximations of Elementary FunctionsHeiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin. [doi]
- Kalas: A Verified, End-To-End Compiler for a Choreographic LanguageJohannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish. [doi]
- Compositional Verification of Interacting Systems Using Event MonadsBohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia. [doi]
- Computational Back-And-Forth Arguments in Constructive Type TheoryDominik Kirst. [doi]
- The Isabelle ENIGMAZarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban. [doi]
- Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler VerificationHrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen. [doi]
- Automatic Test-Case Reduction in Proof Assistants: A Case Study in CoqJason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala. [doi]
- Synthetic Kolmogorov Complexity in CoqYannick Forster 0002, Fabian Kunze, Nils Lauermann. [doi]
- Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in CombinatoricsChelsea Edmonds, Lawrence C. Paulson. [doi]
- A Verified Cyclicity Checker: For Theories with Overloaded ConstantsArve Gengelbach, Johannes Åman Pohjola. [doi]
- Refinement of Parallel Algorithms down to LLVMPeter Lammich. [doi]
- Formalising Szemerédi's Regularity Lemma in LeanYaël Dillies, Bhavik Mehta. [doi]
- Accelerating Verified-Compiler Development with a Verified Rewriting EngineJason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala. [doi]
- Formalizing the Divergence Theorem and the Cauchy Integral Formula in LeanYury Kudryashov. [doi]
- A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)Jagadish Bapanapally, Ruben Gamboa. [doi]
- Candle: A Verified Implementation of HOL LightOskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell. [doi]
- User Interface Design in the HolPy Theorem Prover (Invited Talk)Bohua Zhan. [doi]
- Formalizing the Ring of Adèles of a Global FieldMaría Inés de Frutos-Fernández. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Mechanizing Soundness of Off-Policy EvaluationJared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas. [doi]
- Formalized functional analysis with semilinear mapsFrédéric Dupuis, Robert Y. Lewis, Heather Macbeth. [doi]
- Formalizing Algorithmic Bounds in the Query Model in EasyCryptAlley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu. [doi]
- Formalization of Randomized Approximation Algorithms for Frequency MomentsEmin Karayel. [doi]
- The Zoo of Lambda-Calculus Reduction Strategies, And CoqMalgorzata Biernacka, Witold Charatonik, Tomasz Drab. [doi]
- Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof AssistantNicolas Magaud. [doi]
- Undecidability of Dyadic First-Order Logic in CoqJohannes Hostert, Andrej Dudenhefner, Dominik Kirst. [doi]
- Use and Abuse of Instance Parameters in the Lean Mathematical LibraryAnne Baanen. [doi]
- Seventeen Provers Under the HammerMartin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel. [doi]