LIPIcs, Volume 237, ITP 2022

• June Andronick and Leonardo de Moura LIPIcs, Volume 237, ITP 2022, Complete Volume 10.4230/LIPIcs.ITP.2022
• June Andronick and Leonardo de Moura Front Matter, Table of Contents, Preface, Conference Organization 10.4230/LIPIcs.ITP.2022.0
• Amy Felty Modelling and Verifying Properties of Biological Neural Networks (Invited Talk) 10.4230/LIPIcs.ITP.2022.1
• Bohua Zhan User Interface Design in the HolPy Theorem Prover (Invited Talk) 10.4230/LIPIcs.ITP.2022.2
• Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell Candle: A Verified Implementation of HOL Light 10.4230/LIPIcs.ITP.2022.3
• Anne Baanen Use and Abuse of Instance Parameters in the Lean Mathematical Library 10.4230/LIPIcs.ITP.2022.4
• Jagadish Bapanapally and Ruben Gamboa A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R) 10.4230/LIPIcs.ITP.2022.5
• Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin Dandelion: Certified Approximations of Elementary Functions 10.4230/LIPIcs.ITP.2022.6
• Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab The Zoo of Lambda-Calculus Reduction Strategies, And Coq 10.4230/LIPIcs.ITP.2022.7
• Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel Seventeen Provers Under the Hammer 10.4230/LIPIcs.ITP.2022.8
• Yaël Dillies and Bhavik Mehta Formalising Szemerédi’s Regularity Lemma in Lean 10.4230/LIPIcs.ITP.2022.9
• Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth Formalized functional analysis with semilinear maps 10.4230/LIPIcs.ITP.2022.10
• Chelsea Edmonds and Lawrence C. Paulson Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics 10.4230/LIPIcs.ITP.2022.11
• Yannick Forster, Fabian Kunze, and Nils Lauermann Synthetic Kolmogorov Complexity in Coq 10.4230/LIPIcs.ITP.2022.12
• Asta Halkjær From and Frederik Krogsdal Jacobsen Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL 10.4230/LIPIcs.ITP.2022.13
• María Inés de Frutos-Fernández Formalizing the Ring of Adèles of a Global Field 10.4230/LIPIcs.ITP.2022.14
• Arve Gengelbach and Johannes Åman Pohjola A Verified Cyclicity Checker: For Theories with Overloaded Constants 10.4230/LIPIcs.ITP.2022.15
• Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban The Isabelle ENIGMA 10.4230/LIPIcs.ITP.2022.16
• Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala Accelerating Verified-Compiler Development with a Verified Rewriting Engine 10.4230/LIPIcs.ITP.2022.17
• Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq 10.4230/LIPIcs.ITP.2022.18
• Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst Undecidability of Dyadic First-Order Logic in Coq 10.4230/LIPIcs.ITP.2022.19
• Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification 10.4230/LIPIcs.ITP.2022.20
• Emin Karayel Formalization of Randomized Approximation Algorithms for Frequency Moments 10.4230/LIPIcs.ITP.2022.21
• Dominik Kirst Computational Back-And-Forth Arguments in Constructive Type Theory 10.4230/LIPIcs.ITP.2022.22
• Yury Kudryashov Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean 10.4230/LIPIcs.ITP.2022.23
• Peter Lammich Refinement of Parallel Algorithms down to LLVM 10.4230/LIPIcs.ITP.2022.24
• Nicolas Magaud Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant 10.4230/LIPIcs.ITP.2022.25
• Karol Pąk and Cezary Kaliszyk Formalizing a Diophantine Representation of the Set of Prime Numbers 10.4230/LIPIcs.ITP.2022.26
• Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish Kalas: A Verified, End-To-End Compiler for a Choreographic Language 10.4230/LIPIcs.ITP.2022.27
• Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos Deeper Shallow Embeddings 10.4230/LIPIcs.ITP.2022.28
• Kazuhiko Sakaguchi Reflexive Tactics for Algebra, Revisited 10.4230/LIPIcs.ITP.2022.29
• Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu Formalizing Algorithmic Bounds in the Query Model in EasyCrypt 10.4230/LIPIcs.ITP.2022.30
• Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun Formalization of a Stochastic Approximation Theorem 10.4230/LIPIcs.ITP.2022.31
• Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas Mechanizing Soundness of Off-Policy Evaluation 10.4230/LIPIcs.ITP.2022.32
• Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia Compositional Verification of Interacting Systems Using Event Monads 10.4230/LIPIcs.ITP.2022.33