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