Proceedings

The conference proceedings were published in the LIPIcs series (“Leibniz International Proceedings in Informatics”)

Invited Speakers

Amy Felty

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.

Bohua Zhan

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.

List of Accepted Papers

• Accelerating Verified-Compiler Development with a Verified Rewriting Engine, Jason Gross, Andres Erbsen, Miraya Poddar-Agrawal, Jade Philipoom, Adam Chlipala
• A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r), Jagadish Bapanapally, Ruben Gamboa
• Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq, Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
• A Verified Cyclicity Checker, Arve Gengelbach, Johannes Åman Pohjola
• Candle: A Verified Implementation of HOL Light, Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
• Compositional Verification of Interacting Systems using Event Monads, Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Ye Hong, Bican Xia
• Computational Back-and-Forth Arguments in Constructive Type Theory, Dominik Kirst
• Dandelion: Certified Approximations of Elementary Functions, Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin
• Deeper Shallow Embeddings, Jacob Prinz, Alex Kavvos, Leonidas Lampropoulos
• 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
• Formalization of Randomized Approximation Algorithms for Frequency Moments, Emin Karayel
• Formalized functional analysis with semilinear maps, Frédéric Dupuis, Robert Lewis, Heather Macbeth
• Formalizing Algorithmic Bounds in the Query Model in EasyCrypt, Alley Stoughton, Carol Chen, Marco Gaboardi, Weihao Qu
• 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
• Formalizing the ring of adèles of a global field, María Inés de Frutos-Fernández
• Formalizing the set of primes as an alternative to the DPRM theorem, Karol Pąk, Cezary Kaliszyk
• Kalas: A Verified, End-to-End Compiler for a Choreographic Language, Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish
• Mechanizing Soundness of Off-Policy Evaluation, Jared Yeager, Eliot Moss, Michael Norrish, Philip Thomas
• Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant, Nicolas Magaud
• Refinement of Parallel Algorithms down to LLVM, Peter Lammich
• Reflexive tactics for algebra, revisited, Kazuhiko Sakaguchi
• Seventeen Provers under the Hammer, Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, Makarius Wenzel
• Synthetic Kolmogorov Complexity in Coq, Yannick Forster, Fabian Kunze, Nils Lauermann
• Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification, Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen
• The Isabelle ENIGMA, Zarathustra Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, Josef Urban
• The Zoo of Lambda-Calculus Reduction Strategies, and Coq, Małgorzata Biernacka, Witold Charatonik, Tomasz Drab
• Undecidability of Dyadic First-Order Logic in Coq, Johannes Hostert, Andrej Dudenhefner, Dominik Kirst
• Use and abuse of instance parameters in the Lean mathematical library, Anne Baanen
• Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL, Asta Halkjær From, Frederik Krogsdal Jacobsen

Contact

If you have any problems or questions, please contact us via e-mail at: itp2022@easychair.org