ITP 2021 Accepted Papers

A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks – Andreas Lochbihler. 
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm – Katherine Cordwell, Yong Kiam Tan and André Platzer. 
Unsolvability of the Quintic Formalized in Dependent Type Theory – Sophie Bernard, Cyril Cohen, Assia Mahboubi and Pierre-Yves Strub. 
Verified Double Sided Auctions for Financial Markets – Raja Natarajan, Suneel Sarswat and Abhishek Kr Singh.
Complete Bidirectional Typing for the Calculus of Inductive Constructions – Meven Lennon-Bertrand. 
Syntactic-semantic Form of Mizar Articles – Czesław Byliński, Artur Korniłowicz and Adam Naumowicz. 
Proving Quantum Programs Correct – Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li and Michael Hicks. 
Proof Pearl : Playing with the Tower of Hanoi Formally – Laurent Théry. 
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq – Dominik Kirst and Marc Hermes. 
A formal proof of modal completeness for provability logic – Marco Maggesi and Cosimo Perini Brogi. 
Formalising a Turing-Complete Choreographic Language in Coq – Luís Cruz-Filipe, Fabrizio Montesi and Marco Peressotti. 
A formalization of Dedekind domains and class groups of global fields – Anne Baanen, Sander R. Dahmen, Filippo A. E. Nuccio Mortarino Majno di Capriglio and Ashvni Narayanan.
Formalization of Basic Combinatorics on Words – Stepan Holub and Stepan Starosta. 
Reaching for the Star: Tale of a Monad in Coq – Pierre Nigron and Pierre-Evariste Dagand. 
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq – Lennard Gäher and Fabian Kunze. 
Homotopy Type Theory in Isabelle (Short Paper) – Joshua Chen.
Flexible coinduction in Agda – Luca Ciccone, Francesco Dagnino and Elena Zucca. 
Verified Progress Tracking for Timely Dataflow – Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel. 
A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps – Christian Doczkal. 
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche – Peter Koepke, Adrian De Lon and Anton Lorenzen. 
Itauto: an Extensible Intuitionistic SAT Solver – Frédéric Besson. 
Verifying an HTTP Key-Value Server with Interaction Trees and VST – Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce and Steve Zdancewic.
Value-oriented Legal Argumentation in Isabelle/HOL – Christoph Benzmüller and David Fuenmayor. 
Formalized Haar Measure – Floris van Doorn. 
A graphical user interface framework for formal verification – Edward William Ayers, Mateja Jamnik and William Gowers.
Formal Verification of Termination Criteria for First-Order Recursive Functions – Cesar Munoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andreia B. Avelar da Silva and Thiago M. Ferreira Ramos.
Specifying Message Formats with Contiguity Types – Konrad Slind. 
A Formally Verified Checker for First-Order Proofs – Seulkee Baek. 
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus – Yannick Forster, Fabian Kunze, Gert Smolka and Maximilian Wuttke.