Thirteenth Conference on Interactive Theorem Proving
Haifa, Israel, 2022
The conference proceedings were published in the LIPIcs series (“Leibniz International Proceedings in Informatics”)
9:0010:00

Invited talk: Modelling and Verifying Properties of Biological Neural NetworksAmy Felty 

10:0010:30

General remarks 
11:0012:00

FLoC invited talk 
14:0015:30

Session 1 
Candle: A Verified Implementation of HOL Light Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell 

A Verified Cyclicity Checker Arve Gengelbach, Johannes Åman Pohjola 

Kalas: A Verified, EndtoEnd Compiler for a Choreographic Language Johannes Åman Pohjola, Alejandro GómezLondoño, James Shaker, Michael Norrish 

16:0017:30

Session 2 
Formalized functional analysis with semilinear maps Frédéric Dupuis, Robert Lewis, Heather Macbeth 

Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics Chelsea Edmonds, Lawrence C. Paulson 

Formalization of a Stochastic Approximation Theorem Koundinya Vajjha, Barry Trager, Avraham Shinnar, Vasily Pestun 

17:3018:30

FLoC Panel 
09:0010:30

Session 1 

Refinement of Parallel Algorithms down to LLVM Peter Lammich 

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen 

Dandelion: Certified Approximations of Elementary Functions Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, JeanBaptiste Jeannin 

11:0012:30

Session 2 
Synthetic Kolmogorov Complexity in Coq Yannick Forster, Fabian Kunze, Nils Lauermann 

Formalizing Szemerédi's Regularity Lemma in Lean Bhavik Mehta, Yaël Dillies 

Formalizing the divergence theorem and the Cauchy integral formula in Lean Yury Kudryashov 

14:0015:30

Session 3 
Deeper Shallow Embeddings Jacob Prinz, Alex Kavvos, Leonidas Lampropoulos 

Compositional Verification of Interacting Systems using Event Monads Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Ye Hong, Bican Xia 

Reflexive tactics for algebra, revisited Kazuhiko Sakaguchi 

16:0017:30

Presentation of ITP'23 and ITP Business Meeting 
19:0021:00

FLoC walking tour 
09:0010:30

Session 1 

Formalization of Randomized Approximation Algorithms for Frequency Moments Emin Karayel 

Mechanizing Soundness of OffPolicy Evaluation Jared Yeager, Eliot Moss, Michael Norrish, Philip Thomas 

Formalizing Algorithmic Bounds in the Query Model in EasyCrypt Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu 

11:0012:30

Session 2 
Verifying a Sequent Calculus Prover for FirstOrder Logic with Functions in Isabelle/HOL Asta Halkjær From, Frederik Krogsdal Jacobsen 

Undecidability of Dyadic FirstOrder Logic in Coq Johannes Hostert, Andrej Dudenhefner, Dominik Kirst 

Computational BackandForth Arguments in Constructive Type Theory Dominik Kirst 

14:0015:30

Session 3 
A Complete, MechanicallyVerified Proof of the BanachTarski Theorem in ACL2(r) Jagadish Bapanapally, Ruben Gamboa 

Formalizing the ring of adèles of a global field María Inés de FrutosFernández 

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

16:0017:00

FLoC Plenary Talk 
17:0018:30

FLoC Olympic Games 
9:0010:00

Invited talk: User interface design in the HolPy theorem proverBohua Zhan 

10:0010:30

Session 1 
Accelerating VerifiedCompiler Development with a Verified Rewriting Engine Jason Gross, Andres Erbsen, Miraya PoddarAgrawal, Jade Philipoom, Adam Chlipala 

11:0012:30

Session 2 
The Isabelle ENIGMA Zarathustra Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, Josef Urban 

Seventeen Provers under the Hammer Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, Makarius Wenzel 

Automatic TestCase Reduction in Proof Assistants: A Case Study in Coq Jason Gross, Théo Zimmermann, Miraya PoddarAgrawal, Adam Chlipala 

14:0015:20

Session 3 
Use and abuse of instance parameters in the Lean mathematical library Anne Baanen 

The Zoo of LambdaCalculus Reduction Strategies, and Coq Małgorzata Biernacka, Witold Charatonik, Tomasz Drab 

(SHORT PAPER) Formalizing the set of primes as an alternative to the DPRM theorem Karol Pąk, Cezary Kaliszyk 

15:2015:30

Closing Remarks 
School of Electrical Engineering and Computer Science (EECS), University of Ottawa.
Bio: Amy Felty is a Professor of Computer Science at the University of Ottawa. Her research focuses on formal methods, particularly interactive theorem proving, and she has over 25 years of experience in applying them in various domains. In particular, she has worked in the area of logical frameworks and their application in domains such as programming languages, systems biology, privacy and security, and proof theory. She is on the editorial board of several journals, including the Journal of Automated Reasoning. She is currently the Chair of the National Science and Engineering Research Council of Canada's Discovery Evaluation Group for Computer Science, and Treasurer of the ACM Special Interest Group on Logic and Computation. She holds a Ph.D. in Computer Science from the University of Pennsylvania.
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences.
Bio: Bohua Zhan is an associate research professor at Institute of Software, Chinese Academy of Sciences. He previously worked as postdoc at the Technical University of Munich, and at Massachusetts Institute of Technology. His research interests include proof automation in interactive theorem proving, with applications to program verification and formalization of mathematics. Recently he worked on implementation of a new interactive theorem prover in Python. He also worked on modeling, simulation and verification of embedded systems, and verification of quantum programs.
If you have any problems or questions, please contact us via email at: itp2022@easychair.org