Volume
LIPIcs, Volume 237
13th International Conference on Interactive Theorem Proving (ITP 2022)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP)
Event
ITP 2022, August 7-10, 2022, Haifa, IsraelEditors
Publication Details
- published at: 2022-08-03
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-252-5
- DBLP: db/conf/itp/itp2022
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 237, ITP 2022, Complete Volume
Abstract
LIPIcs, Volume 237, ITP 2022, Complete Volume
Cite as
13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1-602, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{andronick_et_al:LIPIcs.ITP.2022,
title = {{LIPIcs, Volume 237, ITP 2022, Complete Volume}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {1--602},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022},
URN = {urn:nbn:de:0030-drops-167080},
doi = {10.4230/LIPIcs.ITP.2022},
annote = {Keywords: LIPIcs, Volume 237, ITP 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{andronick_et_al:LIPIcs.ITP.2022.0,
author = {Andronick, June and de Moura, Leonardo},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.0},
URN = {urn:nbn:de:0030-drops-167097},
doi = {10.4230/LIPIcs.ITP.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)
Abstract
In this talk, I present a formal model of biological neural networks and discuss the use of model checking and interactive theorem proving to verify some of their properties. Having a formal model can increase our understanding of the behavior and properties of such networks, as well as provide insight into their response to external factors such as disease, medicine, and environmental changes. We focus on neuronal micro-networks, considering properties of single neurons as well as properties of slightly larger ones called archetypes, which represent specific computational functions. Archetypes, in turn, represent the building blocks of larger more complicated neuronal circuits. I first present work by colleagues on a model checking approach, and then present our joint work on a newer theorem proving approach. Using interactive theorem proving allows us to generalize the kinds of properties that we can prove. This work is joint with Abdorrahim Bahrami and Elisabetta De Maria.
Cite as
Amy Felty. Modelling and Verifying Properties of Biological Neural Networks (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{felty:LIPIcs.ITP.2022.1,
author = {Felty, Amy},
title = {{Modelling and Verifying Properties of Biological Neural Networks}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.1},
URN = {urn:nbn:de:0030-drops-167100},
doi = {10.4230/LIPIcs.ITP.2022.1},
annote = {Keywords: Neuronal networks, Model checking, Theorem proving, Coq}
}
Document
Invited Talk
User Interface Design in the HolPy Theorem Prover (Invited Talk)
Abstract
HolPy is a new interactive theorem prover implemented in Python. It is designed to achieve a small trusted-code-base with externally checkable proofs, writing proof automation using a Python API, and permit a wide variety of user interfaces for different application scenarios.
In this talk, I will focus on the design of user interfaces in HolPy. While most interactive theorem provers today use text-based user interfaces, there have been several existing work aiming to build point-and-click interfaces where the user perform actions by clicking on part of the goal or choosing from a menu. In our work, we incorporate into the design extensive proof automation and heuristic suggestion mechanisms, allowing construction of proofs on a large scale using this method. We demonstrate the approach in two common scenarios: general-purpose theorem proving and symbolic computation in mathematics.
Cite as
Bohua Zhan. User Interface Design in the HolPy Theorem Prover (Invited Talk). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{zhan:LIPIcs.ITP.2022.2,
author = {Zhan, Bohua},
title = {{User Interface Design in the HolPy Theorem Prover}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.2},
URN = {urn:nbn:de:0030-drops-167117},
doi = {10.4230/LIPIcs.ITP.2022.2},
annote = {Keywords: Proof assistants, User interface, Proof automation}
}
Document
Candle: A Verified Implementation of HOL Light
Abstract
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically: a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end correctness theorem that guarantees the soundness of the entire system down to the machine code that executes at runtime. Our theorem states that every exported fact produced by this machine-code program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL) that executes the CakeML compiler internally. Throughout this work, we have strived to make the REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end, we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of the work described in this paper has been carried out in the HOL4 theorem prover.
Cite as
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2022.3,
author = {Abrahamsson, Oskar and Myreen, Magnus O. and Kumar, Ramana and Sewell, Thomas},
title = {{Candle: A Verified Implementation of HOL Light}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {3:1--3:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.3},
URN = {urn:nbn:de:0030-drops-167126},
doi = {10.4230/LIPIcs.ITP.2022.3},
annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
Document
Use and Abuse of Instance Parameters in the Lean Mathematical Library
Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Cite as
Anne Baanen. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{baanen:LIPIcs.ITP.2022.4,
author = {Baanen, Anne},
title = {{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4},
URN = {urn:nbn:de:0030-drops-167131},
doi = {10.4230/LIPIcs.ITP.2022.4},
annote = {Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover}
}
Document
A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)
Abstract
This paper presents a formal proof of the Banach-Tarski theorem in ACL2(r). The Banach-Tarski theorem states that a unit ball can be partitioned into a finite number of pieces that can be rotated to form two identical copies of the ball. We have formalized 3D rotations and generated a free group of 3D rotations of rank 2. In prior work, the non-denumerability of the reals was proved in ACL2 (r), and a version of the Axiom of Choice that can consistently select a representative element from an equivalence class was introduced in ACL2 version 3.1. Using the free group of rotations, and this prior work, we show that the unit sphere can be decomposed into two sets, each equivalent to the original sphere. Then we show that the unit ball except for the origin can be decomposed into two sets each equivalent to the original ball by mapping the points of the unit ball to the points on the sphere. Finally, we handle the origin by rotating the unit ball around an axis such that the origin falls inside the sphere. Seemingly paradoxically, the construction results in two copies of the unit ball.
Cite as
Jagadish Bapanapally and Ruben Gamboa. A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R). In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bapanapally_et_al:LIPIcs.ITP.2022.5,
author = {Bapanapally, Jagadish and Gamboa, Ruben},
title = {{A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {5:1--5:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.5},
URN = {urn:nbn:de:0030-drops-167142},
doi = {10.4230/LIPIcs.ITP.2022.5},
annote = {Keywords: ACL2(r), Banach-Tarski, Rotations}
}
Document
Dandelion: Certified Approximations of Elementary Functions
Abstract
Elementary function operations such as sin and exp cannot in general be computed exactly on today’s digital computers, and thus have to be approximated. The standard approximations in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified.
This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.
Cite as
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
author = {Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
title = {{Dandelion: Certified Approximations of Elementary Functions}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
URN = {urn:nbn:de:0030-drops-167155},
doi = {10.4230/LIPIcs.ITP.2022.6},
annote = {Keywords: elementary functions, approximation, certificate checking}
}
Document
The Zoo of Lambda-Calculus Reduction Strategies, And Coq
Abstract
We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.
Cite as
Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
author = {Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
title = {{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7},
URN = {urn:nbn:de:0030-drops-167165},
doi = {10.4230/LIPIcs.ITP.2022.7},
annote = {Keywords: Lambda calculus, Reduction strategies, Coq}
}
Document
Seventeen Provers Under the Hammer
Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.
Cite as
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
title = {{Seventeen Provers Under the Hammer}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
URN = {urn:nbn:de:0030-drops-167178},
doi = {10.4230/LIPIcs.ITP.2022.8},
annote = {Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Document
Formalising Szemerédi’s Regularity Lemma in Lean
Abstract
Szemerédi’s Regularity Lemma is a fundamental result in graph theory with extensive applications to combinatorics and number theory. In essence, it says that all graphs can be approximated by well-behaved unions of random bipartite graphs. We present a formalisation in the Lean theorem prover of a strong version of this lemma in which each part of the union must be approximately the same size. This stronger version has not been formalised previously in any theorem prover. Our proof closely follows the pen-and-paper method, allowing our formalisation to provide an explicit upper bound on the number of parts. An application of this lemma is also formalised, namely Roth’s theorem on arithmetic progressions in qualitative form via the triangle removal lemma.
Cite as
Yaël Dillies and Bhavik Mehta. Formalising Szemerédi’s Regularity Lemma in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dillies_et_al:LIPIcs.ITP.2022.9,
author = {Dillies, Ya\"{e}l and Mehta, Bhavik},
title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.9},
URN = {urn:nbn:de:0030-drops-167185},
doi = {10.4230/LIPIcs.ITP.2022.9},
annote = {Keywords: Lean, formalisation, formal proof, graph theory, combinatorics, additive combinatorics, Szemer\'{e}di’s Regularity Lemma, Roth’s Theorem}
}
Document
Formalized functional analysis with semilinear maps
Abstract
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean’s mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.
Cite as
Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10,
author = {Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather},
title = {{Formalized functional analysis with semilinear maps}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.10},
URN = {urn:nbn:de:0030-drops-167191},
doi = {10.4230/LIPIcs.ITP.2022.10},
annote = {Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}
Document
Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
Abstract
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher’s inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher’s inequality.
Cite as
Chelsea Edmonds and Lawrence C. Paulson. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{edmonds_et_al:LIPIcs.ITP.2022.11,
author = {Edmonds, Chelsea and Paulson, Lawrence C.},
title = {{Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.11},
URN = {urn:nbn:de:0030-drops-167204},
doi = {10.4230/LIPIcs.ITP.2022.11},
annote = {Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics}
}
Document
Synthetic Kolmogorov Complexity in Coq
Abstract
We present a generalised, constructive, and machine-checked approach to Kolmogorov complexity in the constructive type theory underlying the Coq proof assistant. By proving that nonrandom numbers form a simple predicate, we obtain elegant proofs of undecidability for random and nonrandom numbers and a proof of uncomputability of Kolmogorov complexity.
We use a general and abstract definition of Kolmogorov complexity and subsequently instantiate it to several definitions frequently found in the literature.
Whereas textbook treatments of Kolmogorov complexity usually rely heavily on classical logic and the axiom of choice, we put emphasis on the constructiveness of all our arguments, however without blurring their essence. We first give a high-level proof idea using classical logic, which can be formalised with Markov’s principle via folklore techniques we subsequently explain. Lastly, we show a strategy how to eliminate Markov’s principle from a certain class of computability proofs, rendering all our results fully constructive.
All our results are machine-checked by the Coq proof assistant, which is enabled by using a synthetic approach to computability: rather than formalising a model of computation, which is well known to introduce a considerable overhead, we abstractly assume a universal function, allowing the proofs to focus on the mathematical essence.
Cite as
Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.ITP.2022.12,
author = {Forster, Yannick and Kunze, Fabian and Lauermann, Nils},
title = {{Synthetic Kolmogorov Complexity in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {12:1--12:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12},
URN = {urn:nbn:de:0030-drops-167219},
doi = {10.4230/LIPIcs.ITP.2022.12},
annote = {Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq}
}
Document
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
Abstract
We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do so as well when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates.
Cite as
Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{from_et_al:LIPIcs.ITP.2022.13,
author = {From, Asta Halkj{\ae}r and Jacobsen, Frederik Krogsdal},
title = {{Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {13:1--13:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.13},
URN = {urn:nbn:de:0030-drops-167221},
doi = {10.4230/LIPIcs.ITP.2022.13},
annote = {Keywords: Isabelle/HOL, SeCaV, First-Order Logic, Prover, Soundness, Completeness}
}
Document
Formalizing the Ring of Adèles of a Global Field
Abstract
The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.
Cite as
María Inés de Frutos-Fernández. Formalizing the Ring of Adèles of a Global Field. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{defrutosfernandez:LIPIcs.ITP.2022.14,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.14},
URN = {urn:nbn:de:0030-drops-167232},
doi = {10.4230/LIPIcs.ITP.2022.14},
annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib}
}
Document
A Verified Cyclicity Checker: For Theories with Overloaded Constants
Abstract
Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.
Cite as
Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15,
author = {Gengelbach, Arve and \r{A}man Pohjola, Johannes},
title = {{A Verified Cyclicity Checker: For Theories with Overloaded Constants}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15},
URN = {urn:nbn:de:0030-drops-167240},
doi = {10.4230/LIPIcs.ITP.2022.15},
annote = {Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL}
}
Document
The Isabelle ENIGMA
Abstract
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.
Cite as
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16,
author = {Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef},
title = {{The Isabelle ENIGMA}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {16:1--16:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.16},
URN = {urn:nbn:de:0030-drops-167253},
doi = {10.4230/LIPIcs.ITP.2022.16},
annote = {Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer}
}
Document
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Abstract
Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000× faster while actually featuring simpler compiler-specific proofs.
Cite as
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, and Adam Chlipala. Accelerating Verified-Compiler Development with a Verified Rewriting Engine. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gross_et_al:LIPIcs.ITP.2022.17,
author = {Gross, Jason and Erbsen, Andres and Philipoom, Jade and Poddar-Agrawal, Miraya and Chlipala, Adam},
title = {{Accelerating Verified-Compiler Development with a Verified Rewriting Engine}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.17},
URN = {urn:nbn:de:0030-drops-167262},
doi = {10.4230/LIPIcs.ITP.2022.17},
annote = {Keywords: compiler verification, rewriting engines, cryptography}
}
Document
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Abstract
As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof-assistant evolution. We present the Coq Bug Minimizer, a tool for reproducing buggy behavior with minimal and standalone files, integrated with coqbot to trigger automatically on failures from Coq’s reverse dependency compatibility testing. Our tool eliminates the overhead of having to download, set up, compile, and then explore and understand large developments, enabling Coq developers to easily obtain modular test-case files for fast experimentation. In this paper, we describe insights about how test-case reduction is different in Coq than in traditional compilers. We expect that our insights will generalize to other proof assistants. We evaluate the Coq Bug Minimizer on over 150 compatibility testing failures. Our tool succeeds in reducing failures to smaller test cases roughly 75% of the time. The minimizer produces a fully standalone test case 89% of the time, and it is on average about one-third the size of the original test. The average reduced test case compiles in 1.25 seconds, with 75% taking under half a second.
Cite as
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gross_et_al:LIPIcs.ITP.2022.18,
author = {Gross, Jason and Zimmermann, Th\'{e}o and Poddar-Agrawal, Miraya and Chlipala, Adam},
title = {{Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.18},
URN = {urn:nbn:de:0030-drops-167273},
doi = {10.4230/LIPIcs.ITP.2022.18},
annote = {Keywords: debugging, automatic test-case reduction, Coq, bug minimizer}
}
Document
Undecidability of Dyadic First-Order Logic in Coq
Abstract
We develop and mechanize compact proofs of the undecidability of various problems for dyadic first-order logic over a small logical fragment. In this fragment, formulas are restricted to only a single binary relation, and a minimal set of logical connectives. We show that validity, satisfiability, and provability, along with finite satisfiability and finite validity are undecidable, by directly reducing from a suitable binary variant of Diophantine constraints satisfiability. Our results improve upon existing work in two ways: First, the reductions are direct and significantly more compact than existing ones. Secondly, the undecidability of the small logic fragment of dyadic first-order logic was not mechanized before. We contribute our mechanization to the Coq Library of Undecidability Proofs, utilizing its synthetic approach to computability theory.
Cite as
Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of Dyadic First-Order Logic in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19,
author = {Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik},
title = {{Undecidability of Dyadic First-Order Logic in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19},
URN = {urn:nbn:de:0030-drops-167280},
doi = {10.4230/LIPIcs.ITP.2022.19},
annote = {Keywords: undecidability, synthetic computability, first-order logic, Coq}
}
Document
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Abstract
Machine-readable specifications for the Armv8 instruction set architecture have become publicly available as part of Arm’s release processes, providing an official and unambiguous source of truth for the semantics of Arm instructions. To date, compiler and machine code verification efforts have made use of unofficial theorem-proving-friendly specifications of Armv8, e.g. CakeML uses an L3-based specification. The validity of these verification efforts hinges upon their unofficial ISA specifications being valid with respect to the official Arm specification.
Leveraging the Sail language ecosystem, we bridge this validation gap by formally verifying that an L3-based specification simulates the official Arm specification using the HOL4 interactive theorem prover. We exercise this simulation by proving a novel compiler correctness result for CakeML with respect to Arm’s official specification of the Armv8.6 A-class instruction set.
Cite as
Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 20:1-20:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kanabar_et_al:LIPIcs.ITP.2022.20,
author = {Kanabar, Hrutvik and Fox, Anthony C. J. and Myreen, Magnus O.},
title = {{Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {20:1--20:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.20},
URN = {urn:nbn:de:0030-drops-167295},
doi = {10.4230/LIPIcs.ITP.2022.20},
annote = {Keywords: Compiler verification, ISA specification, HOL4, interactive theorem proving}
}
Document
Formalization of Randomized Approximation Algorithms for Frequency Moments
Abstract
In 1999 Alon et al. introduced the still active research topic of approximating the frequency moments of a data stream using randomized algorithms with minimal space usage. This includes the problem of estimating the cardinality of the stream elements - the zeroth frequency moment. Higher-order frequency moments provide information about the skew of the data stream which is, for example, critical information for parallel processing. (The k-th frequency moment of a data stream is the sum of the k-th powers of the occurrence counts of each element in the stream.) They introduce both lower bounds and upper bounds on the space complexity of the problems, which were later improved by newer publications. The algorithms have guaranteed success probabilities and accuracies without making any assumptions on the input distribution. They are an interesting use case for formal verification because their correctness proofs require a large body of deep results from algebra, analysis and probability theory. This work reports on the formal verification of three algorithms for the approximation of F₀, F₂ and F_k for k ≥ 3. The results include the identification of significantly simpler algorithms with the same runtime and space complexities as the previously known ones as well as the development of several reusable components, such as a formalization of universal hash families, amplification methods for randomized algorithms, a model for one-pass data stream algorithms or a generic flexible encoding library for the verification of space complexities.
Cite as
Emin Karayel. Formalization of Randomized Approximation Algorithms for Frequency Moments. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{karayel:LIPIcs.ITP.2022.21,
author = {Karayel, Emin},
title = {{Formalization of Randomized Approximation Algorithms for Frequency Moments}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.21},
URN = {urn:nbn:de:0030-drops-167308},
doi = {10.4230/LIPIcs.ITP.2022.21},
annote = {Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments}
}
Document
Computational Back-And-Forth Arguments in Constructive Type Theory
Abstract
The back-and-forth method is a well-known technique to establish isomorphisms of countable structures. In this proof pearl, we formalise this method abstractly in the framework of constructive type theory, emphasising the computational interpretation of the constructed isomorphisms. As prominent instances, we then deduce Cantor’s and Myhill’s isomorphism theorems on dense linear orders and one-one interreducible sets, respectively. By exploiting the symmetry of the abstract argument, our approach yields a particularly compact mechanisation of the method itself as well as its two instantiations, all implemented using the Coq proof assistant. As adequate for a proof pearl, we attempt to make the text and mechanisation accessible for a general mathematical audience.
Cite as
Dominik Kirst. Computational Back-And-Forth Arguments in Constructive Type Theory. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 22:1-22:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kirst:LIPIcs.ITP.2022.22,
author = {Kirst, Dominik},
title = {{Computational Back-And-Forth Arguments in Constructive Type Theory}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {22:1--22:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.22},
URN = {urn:nbn:de:0030-drops-167311},
doi = {10.4230/LIPIcs.ITP.2022.22},
annote = {Keywords: back-and-forth method, computable isomorphisms, Coq}
}
Document
Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean
Abstract
I formalize a version of the divergence theorem for a function on a rectangular box that does not assume regularity of individual partial derivatives, only Fréchet differentiability of the vector field and integrability of its divergence. Then I use this theorem to prove the Cauchy-Goursat theorem (for some simple domains) and bootstrap complex analysis in the Lean mathematical library. The main tool is the GP-integral, a version of the Henstock-Kurzweil integral introduced by J. Mawhin in 1981. The divergence theorem for this integral does not require integrability of the divergence.
Cite as
Yury Kudryashov. Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kudryashov:LIPIcs.ITP.2022.23,
author = {Kudryashov, Yury},
title = {{Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.23},
URN = {urn:nbn:de:0030-drops-167326},
doi = {10.4230/LIPIcs.ITP.2022.23},
annote = {Keywords: divergence theorem, Green’s theorem, Gauge integral, Cauchy integral formula, Cauchy-Goursat theorem, complex analysis}
}
Document
Refinement of Parallel Algorithms down to LLVM
Abstract
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms' performance is competitive with their counterparts implemented in C/C++. Our approach is backwards compatible with the Isabelle Refinement Framework, such that existing sequential formalizations can easily be adapted or re-used. As case study, we verify a parallel quicksort algorithm, and show that it performs on par with its C++ implementation, and is competitive to state-of-the-art parallel sorting algorithms.
Cite as
Peter Lammich. Refinement of Parallel Algorithms down to LLVM. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{lammich:LIPIcs.ITP.2022.24,
author = {Lammich, Peter},
title = {{Refinement of Parallel Algorithms down to LLVM}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.24},
URN = {urn:nbn:de:0030-drops-167333},
doi = {10.4230/LIPIcs.ITP.2022.24},
annote = {Keywords: Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM}
}
Document
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant
Abstract
We formally implement the smallest three-dimensional projective space PG(3,2) in the Coq proof assistant. This projective space features 15 points and 35 lines, related by an incidence relation. We define points and lines as two plain datatypes (one with 15 constructors for points, and one with 35 constructors for lines) and the incidence relation as a boolean function, instead of using the well-known coordinate-based approach relying on GF(2)⁴. We prove that this implementation actually verifies all the usual properties of three-dimensional projective spaces. We then use an oracle to compute some characteristic subsets of objects of PG(3,2), namely spreads and packings. We formally verify that these computed objects exactly correspond to the spreads and packings of PG(3,2). For spreads, this means identifying 56 specific sets of 5 lines among 360 360 (= 15× 14× 13× 12× 11) possible ones. We then classify them, showing that the 56 spreads of PG(3,2) are all isomorphic whereas the 240 packings of PG(3,2) can be classified into two distinct classes of 120 elements. Proving these results requires partially automating the generation of some large specification files as well as some even larger proof scripts. Overall, this work can be viewed as an example of a large-scale combination of interactive and automated specifications and proofs. It is also a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).
Cite as
Nicolas Magaud. Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{magaud:LIPIcs.ITP.2022.25,
author = {Magaud, Nicolas},
title = {{Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {25:1--25:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.25},
URN = {urn:nbn:de:0030-drops-167349},
doi = {10.4230/LIPIcs.ITP.2022.25},
annote = {Keywords: Coq, projective geometry, finite models, spreads, packings, PG(3, 2)}
}
Document
Formalizing a Diophantine Representation of the Set of Prime Numbers
Abstract
The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert’s 10th problem. Almost three decades of work on the problem have resulted in several equally surprising results. These include the existence of diophantine equations with a reduced number of variables, as well as the explicit construction of polynomials that represent specific sets, in particular the set of primes. In this work, we formalize these constructions in the Mizar system. We focus on the set of prime numbers and its explicit representation using 10 variables. It is the smallest representation known today. For this, we show that the exponential function is diophantine, together with the same properties for the binomial coefficient and factorial. This formalization is the next step in the research on formal approaches to diophantine sets following the DPRM theorem.
Cite as
Karol Pąk and Cezary Kaliszyk. Formalizing a Diophantine Representation of the Set of Prime Numbers. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 26:1-26:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{pak_et_al:LIPIcs.ITP.2022.26,
author = {P\k{a}k, Karol and Kaliszyk, Cezary},
title = {{Formalizing a Diophantine Representation of the Set of Prime Numbers}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {26:1--26:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.26},
URN = {urn:nbn:de:0030-drops-167350},
doi = {10.4230/LIPIcs.ITP.2022.26},
annote = {Keywords: DPRM theorem, Polynomial reduction, prime numbers}
}
Document
Kalas: A Verified, End-To-End Compiler for a Choreographic Language
Abstract
Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this paper, we present a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. This work uses the verified CakeML compiler and Hol4 proof assistant, allowing for concrete executable implementations and statements of correctness at the machine code level for multiple architectures.
Cite as
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27,
author = {Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael},
title = {{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27},
URN = {urn:nbn:de:0030-drops-167368},
doi = {10.4230/LIPIcs.ITP.2022.27},
annote = {Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification}
}
Document
Deeper Shallow Embeddings
Abstract
Deep and shallow embeddings are two popular techniques for embedding a language in a host language with complementary strengths and weaknesses. In a deep embedding, embedded constructs are defined as data in the host: this allows for syntax manipulation and facilitates metatheoretic reasoning, but is challenging to implement - especially in the case of dependently typed embedded languages. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them quite straightforward to implement, but limits their use in practice.
In this paper, we attempt to bridge the gap between the two, by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.
Cite as
Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos. Deeper Shallow Embeddings. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28,
author = {Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
title = {{Deeper Shallow Embeddings}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.28},
URN = {urn:nbn:de:0030-drops-167379},
doi = {10.4230/LIPIcs.ITP.2022.28},
annote = {Keywords: type theory, shallow embedding, deep embedding, Agda}
}
Document
Reflexive Tactics for Algebra, Revisited
Abstract
Computational reflection allows us to turn verified decision procedures into efficient automated reasoning tools in proof assistants. The typical applications of such methodology include decidable algebraic theories such as equational theories of commutative rings and lattices. However, such existing tools are known not to cooperate with packed classes, a methodology to define mathematical structures in dependent type theory, that allows for the sharing of vocabulary across the inheritance hierarchy. Moreover, such tools do not support homomorphisms whose domain and codomain types may differ. This paper demonstrates how to implement reflexive tactics that support packed classes and homomorphisms. As applications of our methodology, we adapt the ring and field tactics of Coq to the commutative ring and field structures of the Mathematical Components library, and apply the resulting tactics to the formal proof of the irrationality of ζ(3) by Chyzak, Mahboubi, and Sibut-Pinote. As a result, the lines of code in the proof scripts have been reduced by 8%, and the time required for proof checking has been decreased by 27%.
Cite as
Kazuhiko Sakaguchi. Reflexive Tactics for Algebra, Revisited. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{sakaguchi:LIPIcs.ITP.2022.29,
author = {Sakaguchi, Kazuhiko},
title = {{Reflexive Tactics for Algebra, Revisited}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {29:1--29:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.29},
URN = {urn:nbn:de:0030-drops-167385},
doi = {10.4230/LIPIcs.ITP.2022.29},
annote = {Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection}
}
Document
Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Abstract
We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm’s queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm’s input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework.
Cite as
Alley Stoughton, Carol Chen, Marco Gaboardi, and Weihao Qu. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30,
author = {Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao},
title = {{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {30:1--30:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.30},
URN = {urn:nbn:de:0030-drops-167399},
doi = {10.4230/LIPIcs.ITP.2022.30},
annote = {Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt}
}
Document
Formalization of a Stochastic Approximation Theorem
Abstract
Stochastic approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown and direct observations are corrupted by noise. These algorithms are useful, for instance, for root-finding and function minimization when the target function or model is not directly known. Originally introduced in a 1951 paper by Robbins and Monro, the field of Stochastic approximation has grown enormously and has come to influence application domains from adaptive signal processing to artificial intelligence. As an example, the Stochastic Gradient Descent algorithm which is ubiquitous in various subdomains of Machine Learning is based on stochastic approximation theory. In this paper, we give a formal proof (in the Coq proof assistant) of a general convergence theorem due to Aryeh Dvoretzky [Dvoretzky, 1956] (proven in 1956) which implies the convergence of important classical methods such as the Robbins-Monro and the Kiefer-Wolfowitz algorithms. In the process, we build a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.
Cite as
Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun. Formalization of a Stochastic Approximation Theorem. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{vajjha_et_al:LIPIcs.ITP.2022.31,
author = {Vajjha, Koundinya and Trager, Barry and Shinnar, Avraham and Pestun, Vasily},
title = {{Formalization of a Stochastic Approximation Theorem}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {31:1--31:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.31},
URN = {urn:nbn:de:0030-drops-167402},
doi = {10.4230/LIPIcs.ITP.2022.31},
annote = {Keywords: Formal Verification, Stochastic Approximation, Stochastic Processes, Probability Theory, Optimization Algorithms}
}
Document
Mechanizing Soundness of Off-Policy Evaluation
Abstract
There are reinforcement learning scenarios - e.g., in medicine - where we are compelled to be as confident as possible that a policy change will result in an improvement before implementing it. In such scenarios, we can employ off-policy evaluation (OPE). The basic idea of OPE is to record histories of behaviors under the current policy, and then develop an estimate of the quality of a proposed new policy, seeing what the behavior would have been under the new policy. As we are evaluating the policy without actually using it, we have the "off-policy" of OPE. Applying a concentration inequality to the estimate, we derive a confidence interval for the expected quality of the new policy. If the confidence interval lies above that of the current policy, we can change policies with high confidence that we will do no harm.
We focus here on the mathematics of this method, by mechanizing the soundness of off-policy evaluation. A natural side effect of the mechanization is both to clarify all the result’s mathematical assumptions and preconditions, and to further develop HOL4’s library of verified statistical mathematics, including concentration inequalities. Of more significance, the OPE method relies on importance sampling, whose soundness we prove using a measure-theoretic approach. In fact, we generalize the standard result, showing it for contexts comprising both discrete and continuous probability distributions.
Cite as
Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas. Mechanizing Soundness of Off-Policy Evaluation. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{yeager_et_al:LIPIcs.ITP.2022.32,
author = {Yeager, Jared and Moss, J. Eliot B. and Norrish, Michael and Thomas, Philip S.},
title = {{Mechanizing Soundness of Off-Policy Evaluation}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.32},
URN = {urn:nbn:de:0030-drops-167413},
doi = {10.4230/LIPIcs.ITP.2022.32},
annote = {Keywords: Formal Methods, HOL4, Reinforcement Learning, Off-Policy Evaluation, Concentration Inequality, Hoeffding}
}
Document
Compositional Verification of Interacting Systems Using Event Monads
Abstract
Large software systems are usually divided into multiple components that interact with each other. How to verify interacting components in a modular way is one of the major problems in formal verification. In many cases, interaction between components can be modeled asynchronously, where events are sent without requiring a response in order to continue with execution of the component. In this paper, we propose a lightweight, event-based framework for verification of components with asynchronous interaction. We define event monads and event systems, and a Hoare logic-style calculus for reasoning about them. The framework is implemented in Isabelle and applied to several case studies, including models for distributed computing, cache-coherence protocols, and verification of partition scheduling in a real-time operating system.
Cite as
Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, and Bican Xia. Compositional Verification of Interacting Systems Using Event Monads. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{zhan_et_al:LIPIcs.ITP.2022.33,
author = {Zhan, Bohua and Lv, Yi and Wang, Shuling and Zhao, Gehang and Hao, Jifeng and Ye, Hong and Xia, Bican},
title = {{Compositional Verification of Interacting Systems Using Event Monads}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {33:1--33:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.33},
URN = {urn:nbn:de:0030-drops-167420},
doi = {10.4230/LIPIcs.ITP.2022.33},
annote = {Keywords: Hoare Logic, Compositional Verification, Events}
}