Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics

Chelsea Edmonds and Lawrence C. Paulson

The Isabelle ENIGMA

Zarathustra Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock and Josef Urban

Compositional Verification of Interacting Systems Using Event Monads

Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Ye Hong and Bican Xia

(Invited) User Interface Design in the HolPy Theorem Prover

Bohua Zhan

Accelerating Verified-Compiler Development with a Verified Rewriting Engine

Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal and Adam Chlipala

Mechanizing Soundness of off-Policy Evaluation

Jared Yeager, Eliot Moss, Michael Norrish and Philip Thomas

Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant

Nicolas Magaud

Computational Back-and-Forth Arguments in Constructive Type Theory

Dominik Kirst

Undecidability of Dyadic First-Order Logic in Coq

Johannes Hostert, Andrej Dudenhefner and Dominik Kirst

Use and Abuse of Instance Parameters in Mathlib

Anne Baanen

A Verified Cyclicity Checker. For Theories with Overloaded Constants

Arve Gengelbach and Johannes Åman Pohjola

One-Dimensional Isocrystsals

Frédéric Dupuis, Robert Lewis and Heather Macbeth

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification

Hrutvik Kanabar, Anthony Fox and Magnus Myreen

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt

Alley Stoughton, Carol Chen, Marco Gaboardi and Weihao Qu

The Zoo of Lambda-Calculus Reduction Strategies, and Coq

Małgorzata Biernacka, Witold Charatonik and Tomasz Drab

Refinement of Parallel Algorithms down to LLVM

Peter Lammich

Dandelion: Certified Approximations of Elementary Functions

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova and Jean-Baptiste Jeannin

Formalization of a Stochastic Approximation Theorem

Koundinya Vajjha, Barry Trager, Avraham Shinnar and Vasily Pestun

A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)

Jagadish Bapanapally and Ruben Gamboa

Formalization of Randomized Approximation Algorithms for Frequency Moments

Emin Karayel

Automatic Test-Case Reduction in Proof Assistants: a Case Study in Coq

Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal and Adam Chlipala