Volume
LIPIcs, Volume 268
14th International Conference on Interactive Theorem Proving (ITP 2023)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP)
Event
ITP 2023, July 31 to August 4, 2023, Białystok, PolandEditors
Publication Details
- published at: 2023-07-26
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-284-6
- DBLP: db/conf/itp/itp2023
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 268, ITP 2023, Complete Volume
Abstract
LIPIcs, Volume 268, ITP 2023, Complete Volume
Cite as
14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{naumowicz_et_al:LIPIcs.ITP.2023,
title = {{LIPIcs, Volume 268, ITP 2023, Complete Volume}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {1--660},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023},
URN = {urn:nbn:de:0030-drops-183747},
doi = {10.4230/LIPIcs.ITP.2023},
annote = {Keywords: LIPIcs, Volume 268, ITP 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{naumowicz_et_al:LIPIcs.ITP.2023.0,
author = {Naumowicz, Adam and Thiemann, Ren\'{e}},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.0},
URN = {urn:nbn:de:0030-drops-183755},
doi = {10.4230/LIPIcs.ITP.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
Abstract
In this talk, I will present an overview of recent formalisations, in the interactive theorem prover Isabelle/HOL, of significant theorems in additive combinatorics, an area of combinatorial number theory. The formalisations of these theorems were the first in any proof assistant to my knowledge. For each of these theorems, I will discuss selected aspects of the formalisation process, focussing on observations on our treatment of certain mathematical arguments when translated into Isabelle/HOL and our overall formalisation experience with Isabelle/HOL for this area of mathematics.
Cite as
Angeliki Koutsoukou-Argyraki. Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{koutsoukouargyraki:LIPIcs.ITP.2023.1,
author = {Koutsoukou-Argyraki, Angeliki},
title = {{Formalisation of Additive Combinatorics in Isabelle/HOL}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.1},
URN = {urn:nbn:de:0030-drops-183760},
doi = {10.4230/LIPIcs.ITP.2023.1},
annote = {Keywords: Additive combinatorics, additive number theory, combinatorial number theory, formalisation of mathematics, interactive theorem proving, proof assistants, Isabelle/HOL}
}
Document
Invited Talk
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
Abstract
In program verification, it is common to embed a high-level object logic into the meta logic of a proof assistant to hide low-level aspects of the verification. To verify imperative and concurrent programs, separation logic hides explicit reasoning about heaps and pointer disjointness. To verify programs with cyclic features such as modules or higher-order state, modal logic provides modalities to hide explicit reasoning about step-indices that are used to stratify recursion.
The meta logic of proof assistants such as Coq is well suited to embed high-level object logics and prove their soundness. However, proof assistants such as Coq do not have native infrastructure to facilitate proofs in embedded logics - their proof contexts and built-in tactics for interactive and automated proofs are tailored to the connectives of the meta logic, and do not extend to those of the object logic. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic.
In this talk I will describe our work in the Iris project to address this problem - first for interactive proofs, and then for semi-automated proofs. The Iris Proof Mode provides high-level tactics for interactive proofs in higher-order concurrent separation logic with modalities. Recent work on RefinedC and Diaframe have built on top of the Iris Proof Mode to obtain proof automation for low-level C programs and fine-grained concurrent programs.
Cite as
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{krebbers:LIPIcs.ITP.2023.2,
author = {Krebbers, Robbert},
title = {{Interactive and Automated Proofs in Modal Separation Logic}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.2},
URN = {urn:nbn:de:0030-drops-183770},
doi = {10.4230/LIPIcs.ITP.2023.2},
annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq}
}
Document
A Formal Analysis of RANKING
Abstract
We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all combinatorial proofs of the algorithm. Filling that gap constituted the majority of the effort which went into this work. This is despite the algorithm being one of the most studied algorithms and a central result in theoretical computer science. This gap is an example of difficulties in formalising graphical arguments which are ubiquitous in the theory of computing.
Cite as
Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2023.3,
author = {Abdulaziz, Mohammad and Madlener, Christoph},
title = {{A Formal Analysis of RANKING}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {3:1--3:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.3},
URN = {urn:nbn:de:0030-drops-183785},
doi = {10.4230/LIPIcs.ITP.2023.3},
annote = {Keywords: Matching Theory, Formalized Mathematics, Online Algorithms}
}
Document
Fast, Verified Computation for Candle
Abstract
This paper describes how we have added an efficient function for computation to the kernel of the Candle interactive theorem prover. Candle is a CakeML port of HOL Light which we have, in prior work, proved sound w.r.t. the inference rules of the higher-order logic. This paper extends the original implementation and soundness proof with a new kernel function for fast computation. Experiments show that the new computation function is able to speed up certain evaluation proofs by several orders of magnitude.
Cite as
Oskar Abrahamsson and Magnus O. Myreen. Fast, Verified Computation for Candle. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2023.4,
author = {Abrahamsson, Oskar and Myreen, Magnus O.},
title = {{Fast, Verified Computation for Candle}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {4:1--4:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.4},
URN = {urn:nbn:de:0030-drops-183797},
doi = {10.4230/LIPIcs.ITP.2023.4},
annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
Document
Formalizing Functions as Processes
Abstract
We present the first formalization of Milner’s classic translation of the λ-calculus into the π-calculus. It is a challenging result with respect to variables, names, and binders, as it requires one to relate variables and binders of the λ-calculus with names and binders in the π-calculus. We formalize it in Abella, merging the set of variables and the set of names, thus circumventing the challenge and obtaining a neat formalization.
About the translation, we follow Accattoli’s factoring of Milner’s result via the linear substitution calculus, which is a λ-calculus with explicit substitutions and contextual rewriting rules, mediating between the λ-calculus and the π-calculus. Another aim of the formalization is to investigate to which extent the use of contexts in Accattoli’s refinement can be formalized.
Cite as
Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing Functions as Processes. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{accattoli_et_al:LIPIcs.ITP.2023.5,
author = {Accattoli, Beniamino and Blanc, Horace and Sacerdoti Coen, Claudio},
title = {{Formalizing Functions as Processes}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {5:1--5:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.5},
URN = {urn:nbn:de:0030-drops-183800},
doi = {10.4230/LIPIcs.ITP.2023.5},
annote = {Keywords: Lambda calculus, pi calculus, proof assistants, binders, Abella}
}
Document
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic
Abstract
Elliptic curves are fundamental objects in number theory and algebraic geometry, whose points over a field form an abelian group under a geometric addition law. Any elliptic curve over a field admits a Weierstrass model, but prior formal proofs that the addition law is associative in this model involve either advanced algebraic geometry or tedious computation, especially in characteristic two. We formalise in the Lean theorem prover, the type of nonsingular points of a Weierstrass curve over a field of any characteristic and a purely algebraic proof that it forms an abelian group.
Cite as
David Kurniadi Angdinata and Junyan Xu. An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{angdinata_et_al:LIPIcs.ITP.2023.6,
author = {Angdinata, David Kurniadi and Xu, Junyan},
title = {{An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.6},
URN = {urn:nbn:de:0030-drops-183817},
doi = {10.4230/LIPIcs.ITP.2023.6},
annote = {Keywords: formal math, algebraic geometry, elliptic curve, group law, Lean, mathlib}
}
Document
A Proof-Producing Compiler for Blockchain Applications
Abstract
Cairo is a programming language for running decentralized applications (dapps) at scale. Programs written in the Cairo language are compiled to machine code for the Cairo CPU architecture, and cryptographic protocols are used to verify the results of the execution traces efficiently on blockchain. We explain how we have extended the Cairo compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computations with an elliptic curve over a large finite field, as well as their use in the validation of cryptographic signatures.
Cite as
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A Proof-Producing Compiler for Blockchain Applications. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{avigad_et_al:LIPIcs.ITP.2023.7,
author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and Seginer, Yoav and Titelman, Alon},
title = {{A Proof-Producing Compiler for Blockchain Applications}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.7},
URN = {urn:nbn:de:0030-drops-183820},
doi = {10.4230/LIPIcs.ITP.2023.7},
annote = {Keywords: formal verification, smart contracts, interactive proof systems}
}
Document
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
Abstract
The Hindley-Damas-Milner (HDM) system provides polymorphism, a key feature of functional programming languages such as Haskell and OCaml. It does so through a type inference algorithm, whose soundness and completeness have been well-studied and proven both manually (on paper) and mechanically (in a proof assistant). Earlier research has focused on the problem of inferring the type of a top-level expression. Yet, in practice, we also may wish to infer the type of subexpressions, either for the sake of elaboration into an explicitly-typed target language, or for reporting those types back to the programmer. One key difference between these two problems is the treatment of underconstrained types: in the former, unification variables that do not affect the overall type need not be instantiated. However, in the latter, instantiating all unification variables is essential, because unification variables are internal to the algorithm and should not leak into the output.
We present an algorithm for the HDM system that explicitly tracks the scope of all unification variables. In addition to solving the subexpression type reconstruction problem described above, it can be used as a basis for elaboration algorithms, including those that implement elaboration-based features such as type classes. The algorithm implements input and output contexts, as well as the novel concept of full contexts, which significantly simplifies the state-passing of traditional algorithms. The algorithm has been formalised and proven sound and complete using the Coq proof assistant.
Cite as
Roger Bosman, Georgios Karachalias, and Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bosman_et_al:LIPIcs.ITP.2023.8,
author = {Bosman, Roger and Karachalias, Georgios and Schrijvers, Tom},
title = {{No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.8},
URN = {urn:nbn:de:0030-drops-183836},
doi = {10.4230/LIPIcs.ITP.2023.8},
annote = {Keywords: type inference, mechanization, let-polymorphism}
}
Document
Automated Theorem Proving for Metamath
Abstract
Metamath is a proof assistant that keeps surprising outsiders by its combination of a very minimalist design with a large library of advanced results, ranking high on the Freek Wiedijk’s 100 list. In this work, we develop several translations of the Metamath logic and its large set-theoretical library into higher-order and first-order TPTP formats for automated theorem provers (ATPs). We show that state-of-the-art ATPs can prove 68% of the Metamath problems automatically when using the premises that were used in the human-written Metamath proofs. Finally, we add proof reconstruction and premise selection methods and combine the components into the first hammer system for Metamath.
Cite as
Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9,
author = {Carneiro, Mario and Brown, Chad E. and Urban, Josef},
title = {{Automated Theorem Proving for Metamath}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.9},
URN = {urn:nbn:de:0030-drops-183846},
doi = {10.4230/LIPIcs.ITP.2023.9},
annote = {Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery}
}
Document
Reimplementing Mizar in Rust
Abstract
This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "checker" and "analyzer" of Mizar are implemented, which together form the trusted core of Mizar. This is to our knowledge the first and only external implementation of these components. Thanks to the loose coupling of Mizar’s passes, it is possible to use the checker as a drop-in replacement for the original, and we have used this to verify the entire MML in 11.8 minutes on 8 cores, a 4.8× speedup over the original Pascal implementation. Since Mizar is not designed to have a small trusted core, checking Mizar proofs entails following Mizar closely, so our ability to detect bugs is limited. Nevertheless, we were able to find multiple memory errors, four soundness bugs in the original (which were not being exploited in MML), in addition to one non-critical bug which was being exploited in 46 different MML articles. We hope to use this checker as a base for proof export tooling, as well as revitalizing development of the language.
Cite as
Mario Carneiro. Reimplementing Mizar in Rust. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{carneiro:LIPIcs.ITP.2023.10,
author = {Carneiro, Mario},
title = {{Reimplementing Mizar in Rust}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.10},
URN = {urn:nbn:de:0030-drops-183852},
doi = {10.4230/LIPIcs.ITP.2023.10},
annote = {Keywords: Mizar, proof checker, software, Rust}
}
Document
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
Abstract
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing.
Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.
Cite as
Luís Cruz-Filipe and Fabrizio Montesi. Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2023.11,
author = {Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio},
title = {{Now It Compiles! Certified Automatic Repair of Uncompilable Protocols}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.11},
URN = {urn:nbn:de:0030-drops-183867},
doi = {10.4230/LIPIcs.ITP.2023.11},
annote = {Keywords: choreographic programming, theorem proving, compilation, program repair}
}
Document
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
Abstract
The Coq Community Survey 2022 was an online public survey of users of the Coq proof assistant conducted during February 2022. Broadly, the survey asked about use of Coq features, user interfaces, libraries, plugins, and tools, views on renaming Coq and Coq improvements, and also demographic data such as education and experience with Coq and other proof assistants and programming languages. The survey received 466 submitted responses, making it the largest survey of users of an interactive theorem prover (ITP) so far. We present the design of the survey, a summary of key results, and analysis of answers relevant to ITP technology development and usage. In particular, we analyze user characteristics associated with adoption of tools and libraries and make comparisons to adjacent software communities. Notably, we find that experience has significant impact on Coq user behavior, including on usage of tools, libraries, and integrated development environments.
Cite as
Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dealmeidaborges_et_al:LIPIcs.ITP.2023.12,
author = {de Almeida Borges, Ana and Casanueva Art{\'\i}s, Annal{\'\i} and Falleri, Jean-R\'{e}my and Gallego Arias, Emilio Jes\'{u}s and Martin-Dorel, \'{E}rik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Th\'{e}o},
title = {{Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.12},
URN = {urn:nbn:de:0030-drops-183875},
doi = {10.4230/LIPIcs.ITP.2023.12},
annote = {Keywords: Coq, Community, Survey, Statistical Analysis}
}
Document
Formalizing Norm Extensions and Applications to Number Theory
Abstract
The field ℝ of real numbers is obtained from the rational numbers ℚ by taking the completion with respect to the usual absolute value. We then define the complex numbers ℂ as an algebraic closure of ℝ. The p-adic analogue of the real numbers is the field ℚ_p of p-adic numbers, obtained by completing ℚ with respect to the p-adic norm. In this paper, we formalize in Lean 3 the definition of the p-adic analogue of the complex numbers, which is the field ℂ_p of p-adic complex numbers, a field extension of ℚ_p which is both algebraically closed and complete with respect to the extension of the p-adic norm.
More generally, given a field K complete with respect to a nonarchimedean real-valued norm, and an algebraic field extension L/K, we show that there is a unique norm on L extending the given norm on K, with an explicit description.
Building on the definition of ℂ_p, we formalize the definition of the Fontaine period ring B_{HT} and discuss some applications to the theory of Galois representations and to p-adic Hodge theory.
The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat’s Last Theorem.
Cite as
María Inés de Frutos-Fernández. Formalizing Norm Extensions and Applications to Number Theory. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{defrutosfernandez:LIPIcs.ITP.2023.13,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing Norm Extensions and Applications to Number Theory}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.13},
URN = {urn:nbn:de:0030-drops-183880},
doi = {10.4230/LIPIcs.ITP.2023.13},
annote = {Keywords: formal mathematics, Lean, mathlib, algebraic number theory, p-adic analysis, Galois representations, p-adic Hodge theory}
}
Document
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure
Abstract
Verifying the metatheory of a formal system in Coq involves a lot of tedious "infrastructural" reasoning about variable binders. We present Tealeaves, a generic framework for first-order representations of variable binding that can be used to develop this sort of infrastructure once and for all. Given a particular strategy for representing binders concretely, such as locally nameless or de Bruijn indices, Tealeaves allows developers to implement modules of generic infrastructure called backends that end users can simply instantiate to their own syntax. Our framework rests on a novel abstraction of first-order abstract syntax called a decorated traversable monad (DTM) whose equational theory provides reasoning principles that replace tedious induction on terms. To evaluate Tealeaves, we have implemented a multisorted locally nameless backend providing generic versions of the lemmas generated by LNgen. We discuss case studies where we instantiate this generic infrastructure to simply-typed and polymorphic lambda calculi, comparing our approach to other utilities.
Cite as
Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dunn_et_al:LIPIcs.ITP.2023.14,
author = {Dunn, Lawrence and Tannen, Val and Zdancewic, Steve},
title = {{Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.14},
URN = {urn:nbn:de:0030-drops-183891},
doi = {10.4230/LIPIcs.ITP.2023.14},
annote = {Keywords: Coq, category theory, formal metatheory, raw syntax, locally nameless}
}
Document
Closure Properties of General Grammars – Formally Verified
Abstract
We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.
Cite as
Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15,
author = {Dvorak, Martin and Blanchette, Jasmin},
title = {{Closure Properties of General Grammars – Formally Verified}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.15},
URN = {urn:nbn:de:0030-drops-183906},
doi = {10.4230/LIPIcs.ITP.2023.15},
annote = {Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star}
}
Document
Formalising Yoneda Ext in Univalent Foundations
Abstract
Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups [Yoneda, 1954] in homotopy type theory (HoTT) using the Coq-HoTT library. This is an approach to Ext which does not require projective or injective resolutions, though it produces large abelian groups. Using univalence, we show how these Ext groups can be naturally represented in HoTT. We give a novel proof and formalisation of the usual six-term exact sequence via a fibre sequence of 1-types (or groupoids), along with an application. In addition, we discuss our formalisation of the contravariant long exact sequence of Ext, an important computational tool. Along the way we implement and explain the Baer sum of extensions and how Ext is a bifunctor.
Cite as
Jarl G. Taxerås Flaten. Formalising Yoneda Ext in Univalent Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{flaten:LIPIcs.ITP.2023.16,
author = {Flaten, Jarl G. Taxer\r{a}s},
title = {{Formalising Yoneda Ext in Univalent Foundations}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.16},
URN = {urn:nbn:de:0030-drops-183911},
doi = {10.4230/LIPIcs.ITP.2023.16},
annote = {Keywords: homotopy type theory, homological algebra, Yoneda Ext, formalisation, Coq}
}
Document
LISA - A Modern Proof System
Abstract
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We also present early formalization of set theory in LISA, including Cantor’s theorem.
Cite as
Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. LISA - A Modern Proof System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{guilloud_et_al:LIPIcs.ITP.2023.17,
author = {Guilloud, Simon and Gambhir, Sankalp and Kun\v{c}ak, Viktor},
title = {{LISA - A Modern Proof System}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {17:1--17:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.17},
URN = {urn:nbn:de:0030-drops-183922},
doi = {10.4230/LIPIcs.ITP.2023.17},
annote = {Keywords: Proof assistant, First Order Logic, Set Theory}
}
Document
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
Abstract
Higher-order probabilistic programs are used to describe statistical models and machine-learning mechanisms. The programming languages for them are equipped with three features: higher-order functions, sampling, and conditioning. In this paper, we propose an Isabelle/HOL library for probabilistic programs supporting all of those three features. We extend our previous quasi-Borel theory library in Isabelle/HOL. As a basis of the theory, we formalize s-finite kernels, which is considered as a theoretical foundation of first-order probabilistic programs and a key to support conditioning of probabilistic programs. We also formalize the Borel isomorphism theorem which plays an important role in the quasi-Borel theory. Using them, we develop the s-finite measure monad on quasi-Borel spaces. Our extension enables us to describe higher-order probabilistic programs with conditioning directly as an Isabelle/HOL term whose type is that of morphisms between quasi-Borel spaces. We also implement the qbs prover for checking well-typedness of an Isabelle/HOL term as a morphism between quasi-Borel spaces. We demonstrate several verification examples of higher-order probabilistic programs with conditioning.
Cite as
Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{hirata_et_al:LIPIcs.ITP.2023.18,
author = {Hirata, Michikazu and Minamide, Yasuhiko and Sato, Tetsuya},
title = {{Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.18},
URN = {urn:nbn:de:0030-drops-183933},
doi = {10.4230/LIPIcs.ITP.2023.18},
annote = {Keywords: Higher-order probabilistic program, s-finite kernel, Quasi-Borel spaces, Isabelle/HOL}
}
Document
MizAR 60 for Mizar 50
Abstract
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60% of the Mizar theorems in the hammer setting. We also automatically prove 75% of the Mizar theorems when the automated provers are helped by using only the premises used in the human-written Mizar proofs. We describe the methods and large-scale experiments leading to these results. This includes in particular the E and Vampire provers, their ENIGMA and Deepire learning modifications, a number of learning-based premise selection methods, and the incremental loop that interleaves growing a corpus of millions of ATP proofs with training increasingly strong AI/TP systems on them. We also present a selection of Mizar problems that were proved automatically.
Cite as
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19,
author = {Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef},
title = {{MizAR 60 for Mizar 50}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {19:1--19:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.19},
URN = {urn:nbn:de:0030-drops-183942},
doi = {10.4230/LIPIcs.ITP.2023.19},
annote = {Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning}
}
Document
Constructive Final Semantics of Finite Bags
Abstract
Finitely-branching and unlabelled dynamical systems are typically modelled as coalgebras for the finite powerset functor. If states are reachable in multiple ways, coalgebras for the finite bag functor provide a more faithful representation. The final coalgebra of this functor is employed as a denotational domain for the evaluation of such systems. Elements of the final coalgebra are non-wellfounded trees with finite unordered branching, representing the evolution of systems starting from a given initial state.
This paper is dedicated to the construction of the final coalgebra of the finite bag functor in homotopy type theory (HoTT). We first compare various equivalent definitions of finite bags employing higher inductive types, both as sets and as groupoids (in the sense of HoTT). We then analyze a few well-known, classical set-theoretic constructions of final coalgebras in our constructive setting. We show that, in the case of set-based definitions of finite bags, some constructions are intrinsically classical, in the sense that they are equivalent to some weak form of excluded middle. Nevertheless, a type satisfying the universal property of the final coalgebra can be constructed in HoTT employing the groupoid-based definition of finite bags. We conclude by discussing generalizations of our constructions to the wider class of analytic functors.
Cite as
Philipp Joram and Niccolò Veltri. Constructive Final Semantics of Finite Bags. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{joram_et_al:LIPIcs.ITP.2023.20,
author = {Joram, Philipp and Veltri, Niccol\`{o}},
title = {{Constructive Final Semantics of Finite Bags}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {20:1--20:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.20},
URN = {urn:nbn:de:0030-drops-183954},
doi = {10.4230/LIPIcs.ITP.2023.20},
annote = {Keywords: finite bags, final coalgebra, homotopy type theory, Cubical Agda}
}
Document
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq
Abstract
Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of μ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the μ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of μ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.
Cite as
Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{larcheywendling_et_al:LIPIcs.ITP.2023.21,
author = {Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
title = {{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.21},
URN = {urn:nbn:de:0030-drops-183963},
doi = {10.4230/LIPIcs.ITP.2023.21},
annote = {Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml}
}
Document
Group Cohomology in the Lean Community Library
Abstract
Group cohomology is a tool which has become indispensable in a wide range of modern mathematics, like algebraic geometry and algebraic number theory, as well as group theory itself. For example, it allows us to reformulate classical class field theory in cohomological terms; this formulation is essential to landmarks of modern number theory, like Wiles’s proof of Fermat’s Last Theorem. We explore the challenges of formalising group cohomology in the Lean theorem prover in a generality suitable for inclusion in the community library mathlib.
Cite as
Amelia Livingston. Group Cohomology in the Lean Community Library. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{livingston:LIPIcs.ITP.2023.22,
author = {Livingston, Amelia},
title = {{Group Cohomology in the Lean Community Library}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.22},
URN = {urn:nbn:de:0030-drops-183974},
doi = {10.4230/LIPIcs.ITP.2023.22},
annote = {Keywords: formal math, Lean, mathlib, group cohomology, homological algebra}
}
Document
A Formalisation of Gallagher’s Ergodic Theorem
Abstract
Gallagher’s ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking "all or nothing" behaviour. We discuss a formalisation of this result in the Lean theorem prover. As well as being notable in its own right, the result is a key preliminary, required for Koukoulopoulos and Maynard’s stunning recent proof of the Duffin-Schaeffer conjecture.
Cite as
Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{nash:LIPIcs.ITP.2023.23,
author = {Nash, Oliver},
title = {{A Formalisation of Gallagher’s Ergodic Theorem}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {23:1--23:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.23},
URN = {urn:nbn:de:0030-drops-183981},
doi = {10.4230/LIPIcs.ITP.2023.23},
annote = {Keywords: Lean proof assistant, measure theory, metric number theory, ergodicity, Gallagher’s theorem, Duffin-Schaeffer conjecture}
}
Document
An Extensible User Interface for Lean 4
Abstract
Contemporary proof assistants rely on complex automation and process libraries with millions of lines of code. At these scales, understanding the emergent interactions between components can be a serious challenge. One way of managing complexity, long established in informal practice, is through varying external representations. For instance, algebraic notation facilitates term-based reasoning whereas geometric diagrams invoke spatial intuition. Objects viewed one way become much simpler than when viewed differently. In contrast, modern general-purpose ITP systems usually only support limited, textual representations. Treating this as a problem of human-computer interaction, we aim to demonstrate that presentations - UI elements that store references to the objects they are displaying - are a fruitful way of thinking about ITP interface design. They allow us to make headway on two fronts - introspection of prover internals and support for diagrammatic reasoning. To this end we have built an extensible user interface for the Lean 4 prover with an associated ProofWidgets 4 library of presentation-based UI components. We demonstrate the system with several examples including type information popups, structured traces, contextual suggestions, a display for algebraic reasoning, and visualizations of red-black trees. Our interface is already part of the core Lean distribution.
Cite as
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24,
author = {Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel},
title = {{An Extensible User Interface for Lean 4}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {24:1--24:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.24},
URN = {urn:nbn:de:0030-drops-183991},
doi = {10.4230/LIPIcs.ITP.2023.24},
annote = {Keywords: user interfaces, human-computer interaction, Lean}
}
Document
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
Abstract
Decision theory and game theory are both interdisciplinary domains that focus on modelling and {analyzing} decision-making processes. On the one hand, decision theory aims to account for the possible behaviors of an agent with respect to an uncertain situation. It thus provides several frameworks to describe the decision-making processes in this context, including that of belief functions. On the other hand, game theory focuses on multi-agent decisions, typically with probabilistic uncertainty (if any), hence the so-called class of Bayesian games. In this paper, we use the Coq/SSReflect proof assistant to formally prove the results we obtained in [Pierre Pomeret{-}Coquot et al., 2022]. First, we formalize a general theory of belief functions with finite support, and structures and solutions concepts from game theory. On top of that, we extend Bayesian games to the theory of belief functions, so that we obtain a more expressive class of games we refer to as Bel games; it makes it possible to better capture human behaviors with respect to lack of information. Next, we provide three different proofs of an extended version of the so-called Howson-Rosenthal’s theorem, showing that Bel games can be casted into games of complete information, i.e., without any uncertainty. We thus embed this class of games into classical game theory, enabling the use of existing algorithms.
Cite as
Pierre Pomeret-Coquot, Hélène Fargier, and Érik Martin-Dorel. Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pomeretcoquot_et_al:LIPIcs.ITP.2023.25,
author = {Pomeret-Coquot, Pierre and Fargier, H\'{e}l\`{e}ne and Martin-Dorel, \'{E}rik},
title = {{Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.25},
URN = {urn:nbn:de:0030-drops-184001},
doi = {10.4230/LIPIcs.ITP.2023.25},
annote = {Keywords: Game of Incomplete Information, Belief Function Theory, Coq Proof Assistant, SSReflect Proof Language, MathComp Library}
}
Document
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
Abstract
We report on our efforts building a new, large proof-repair dataset and benchmark suite for the Coq proof assistant. The dataset is made up of Git commits from open-source projects with old and new versions of definitions and proofs aligned across commits. Building this dataset has been a significant undertaking, highlighting a number of challenges and gaps in existing infrastructure. We discuss these challenges and gaps, and we provide recommendations for how the proof assistant community can address them. Our hope is to make it easier to build datasets and benchmark suites so that machine-learning tools for proofs will move to target the tasks that matter most and do so equitably across proof assistants.
Cite as
Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{reichel_et_al:LIPIcs.ITP.2023.26,
author = {Reichel, Tom and Henderson, R. Wesley and Touchet, Andrew and Gardner, Andrew and Ringer, Talia},
title = {{Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.26},
URN = {urn:nbn:de:0030-drops-184013},
doi = {10.4230/LIPIcs.ITP.2023.26},
annote = {Keywords: proof repair, datasets, benchmarks, machine learning, formal proof}
}
Document
POSIX Lexing with Bitcoded Derivatives
Abstract
Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string - that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an "aggressive" simplification function that keeps the size of derivatives finitely bounded. Without simplification the size of some derivatives can grow arbitrarily big, resulting in an extremely slow lexing algorithm. In this paper we describe a variant of Sulzmann and Lu’s algorithm: Our variant is a recursive functional program, whereas Sulzmann and Lu’s version involves a fixpoint construction. We (i) prove in Isabelle/HOL that our variant is correct and generates unique POSIX values (no such proof has been given for the original algorithm by Sulzmann and Lu); we also (ii) establish finite bounds for the size of our derivatives.
Cite as
Chengsong Tan and Christian Urban. POSIX Lexing with Bitcoded Derivatives. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{tan_et_al:LIPIcs.ITP.2023.27,
author = {Tan, Chengsong and Urban, Christian},
title = {{POSIX Lexing with Bitcoded Derivatives}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.27},
URN = {urn:nbn:de:0030-drops-184027},
doi = {10.4230/LIPIcs.ITP.2023.27},
annote = {Keywords: POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
}
Document
A Sound and Complete Projection for Global Types
Abstract
Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role.
Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.
Cite as
Dawit Tirore, Jesper Bengtson, and Marco Carbone. A Sound and Complete Projection for Global Types. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{tirore_et_al:LIPIcs.ITP.2023.28,
author = {Tirore, Dawit and Bengtson, Jesper and Carbone, Marco},
title = {{A Sound and Complete Projection for Global Types}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {28:1--28:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.28},
URN = {urn:nbn:de:0030-drops-184039},
doi = {10.4230/LIPIcs.ITP.2023.28},
annote = {Keywords: Session types, Mechanisation, Projection, Coq}
}
Document
Real-Time Double-Ended Queue Verified (Proof Pearl)
Abstract
We present the first verification of the real-time doubled-ended queue by Chuang and Goldberg where all operations take constant time. The main contributions are the full system invariant, the precise definition of all abstraction functions, the structure of the proof and the main lemmas.
Cite as
Balazs Toth and Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{toth_et_al:LIPIcs.ITP.2023.29,
author = {Toth, Balazs and Nipkow, Tobias},
title = {{Real-Time Double-Ended Queue Verified (Proof Pearl)}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {29:1--29:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.29},
URN = {urn:nbn:de:0030-drops-184044},
doi = {10.4230/LIPIcs.ITP.2023.29},
annote = {Keywords: Double-ended queue, data structures, verification, Isabelle}
}
Document
Certifying Higher-Order Polynomial Interpretations
Abstract
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method that is used to prove termination, namely the polynomial interpretation method. In addition, we give a program that processes proof traces containing a high-level description of a termination proof into a formal Coq proof script that can be checked by Coq. We demonstrate the usability of this approach by certifying higher-order polynomial interpretation proofs produced by Wanda, a termination analysis tool for higher-order rewriting.
Cite as
Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{vanderweide_et_al:LIPIcs.ITP.2023.30,
author = {van der Weide, Niels and Vale, Deivid and Kop, Cynthia},
title = {{Certifying Higher-Order Polynomial Interpretations}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {30:1--30:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.30},
URN = {urn:nbn:de:0030-drops-184051},
doi = {10.4230/LIPIcs.ITP.2023.30},
annote = {Keywords: higher-order rewriting, Coq, termination, formalization}
}
Document
Slice Nondeterminism
Abstract
This paper studies a technique for describing and formalising nondeterministic functions, using slice categories. Results of a nondeterministic function are modelled by an object of the slice category over the codomain of the function, which is an indexed family over the codomain. Two such families denote the same set of results if slice morphisms exist between them in both directions. We formulate the category of nondeterministic functions by expressing a set of possible results as an equivalence class of objects. If we allow families to use any indexing set, this category will be equivalent to the category of relations. When we limit ourselves to a smaller universe of indexing sets, we get a subcategory which more closely resembles nondeterministic programs. We compare this category with other representations of the category of relations, and see how many properties can be carried over, such as its product, coproduct and other monoidal structures. We can describe inductive nondeterministic structures by lifting free monads from the category of sets. Moreover, due to the intensional nature of the slice representation, nondeterministic processes are easily represented, such as interleaving concurrency and labelled transition systems. This paper has been formalised in Agda.
Cite as
Niels F. W. Voorneveld. Slice Nondeterminism. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{voorneveld:LIPIcs.ITP.2023.31,
author = {Voorneveld, Niels F. W.},
title = {{Slice Nondeterminism}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.31},
URN = {urn:nbn:de:0030-drops-184063},
doi = {10.4230/LIPIcs.ITP.2023.31},
annote = {Keywords: Category theory, Agda, Slice category, Nondeterministic functions, Powerset}
}
Document
Foundational Verification of Stateful P4 Packet Processing
Abstract
P4 is a standardized programming language for the network data plane. But P4 is not just for routing anymore. As programmable switches support stateful objects, P4 programs move beyond just stateless forwarders into new stateful applications: network telemetry (heavy hitters, DDoS detection, performance monitoring), middleboxes (firewalls, NAT, load balancers, intrusion detection), and distributed services (in-network caching, lock management, conflict detection). The complexity of stateful programs and their richer specifications are beyond what existing P4 program verifiers can handle.
Verifiable P4 is a new interactive verification framework for P4 that (1) allows reasoning about multi-packet properties by specifying the per-packet relation between initial and final states; (2) performs modular verification, especially providing a modular description for stateful objects; (3) is foundational, i.e., with a machine-checked soundness proof with respect to a formal operational semantics of P4_{16} (the current specification of P4) in Coq. In addition, our framework includes a proved-correct reference interpreter.
We demonstrate the framework with the specification and verification of a stateful firewall that uses a sliding-window Bloom filter on a Tofino switch to block (most) unsolicited traffic.
Cite as
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. Foundational Verification of Stateful P4 Packet Processing. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.ITP.2023.32,
author = {Wang, Qinshi and Pan, Mengying and Wang, Shengyi and Doenges, Ryan and Beringer, Lennart and Appel, Andrew W.},
title = {{Foundational Verification of Stateful P4 Packet Processing}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.32},
URN = {urn:nbn:de:0030-drops-184077},
doi = {10.4230/LIPIcs.ITP.2023.32},
annote = {Keywords: Software Defined Networking, Verifiable P4, Stateful data plane programming}
}
Document
Dependently Sorted Theorem Proving for Mathematical Foundations
Abstract
We describe a new meta-logical system for mechanising foundations of mathematics. Using dependent sorts and first order logic, our system (implemented as an LCF-style theorem-prover) improves on the state-of-the-art by providing efficient type-checking, convenient automatic rewriting and interactive proof support. We assess our implementation by axiomatising Lawvere’s Elementary Theory of the Category of Sets (ETCS) [F. William Lawvere, 1964], and Shulman’s Sets, Elements and Relations (SEAR) [Michael Shulman, 2022]. We then demonstrate our system’s ability to perform some basic mathematical constructions such as quotienting, induction and coinduction by constructing integers, lists and colists. We also compare with some existing work on modal model theory done in HOL4 [Yiming Xu and Michael Norrish, 2020]. Using the analogue of type-quantification, we are able to prove a theorem that this earlier work could not. Finally, we show that SEAR can construct sets that are larger than any finite iteration of the power set operation. This shows that SEAR, unlike HOL, can construct sets beyond V_{ω+ω}.
Cite as
Yiming Xu and Michael Norrish. Dependently Sorted Theorem Proving for Mathematical Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{xu_et_al:LIPIcs.ITP.2023.33,
author = {Xu, Yiming and Norrish, Michael},
title = {{Dependently Sorted Theorem Proving for Mathematical Foundations}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {33:1--33:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.33},
URN = {urn:nbn:de:0030-drops-184085},
doi = {10.4230/LIPIcs.ITP.2023.33},
annote = {Keywords: first order logic, sorts, structural set theory, mechanised mathematics, foundation of mathematics, category theory}
}
Document
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)
Abstract
Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL’s ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.
Cite as
Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34,
author = {Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
title = {{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {34:1--34:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.34},
URN = {urn:nbn:de:0030-drops-184092},
doi = {10.4230/LIPIcs.ITP.2023.34},
annote = {Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL}
}
Document
Formalising the Proj Construction in Lean
Abstract
Many objects of interest in mathematics can be studied both analytically and algebraically, while at the same time, it is known that analytic geometry and algebraic geometry generally do not behave the same. However, the famous GAGA theorem asserts that for projective varieties, analytic and algebraic geometries are closely related; the proof of Fermat’s last theorem, for example, uses this technique to transport between the two worlds [Serre, 1955]. A crucial step of proving GAGA is to calculate cohomology of projective space [Neeman, 2007; Godement, 1958], thus I formalise the Proj construction in the Lean theorem prover for any ℕ-graded R-algebra A and construct projective n-space as Proj A[X₀,… , X_n]. This is the first family of non-affine schemes formalised in any theorem prover.
Cite as
Jujian Zhang. Formalising the Proj Construction in Lean. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{zhang:LIPIcs.ITP.2023.35,
author = {Zhang, Jujian},
title = {{Formalising the Proj Construction in Lean}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {35:1--35:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.35},
URN = {urn:nbn:de:0030-drops-184105},
doi = {10.4230/LIPIcs.ITP.2023.35},
annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry}
}
Document
Short Paper
Fermat’s Last Theorem for Regular Primes (Short Paper)
Abstract
We formalise the proof of the first case of Fermat’s Last Theorem for regular primes using the Lean theorem prover and its mathematical library mathlib. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to mathlib.
Cite as
Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 36:1-36:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{best_et_al:LIPIcs.ITP.2023.36,
author = {Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric},
title = {{Fermat’s Last Theorem for Regular Primes}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {36:1--36:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.36},
URN = {urn:nbn:de:0030-drops-184115},
doi = {10.4230/LIPIcs.ITP.2023.36},
annote = {Keywords: Fermat’s Last Theorem, Cyclotomic fields, Interactive theorem proving, Lean}
}
Document
Short Paper
Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
Abstract
The Mizar language and its corresponding proof-checker offers the tactic of definitional expansions in proof skeletons. This apparatus is rather fragile in the case of intensive overloading of notions (which is widely observed e.g. in the field of algebra, but it is also present in the more fundamental set-theory contexts). We propose the extension of this mechanism: the change should offer users the more precise control over expansions via choosing the right definitional variant for the proof under consideration, still letting the authors to retain the more conservative approach. As a rule, the change will affect new Mizar texts, but obviously, it allows also for solving some context conflicts caused by the original approach in the Mizar repository. The usefulness of our approach is shown by a number of experiments carried out within MML, which is also affected by the change.
Cite as
Adam Grabowski and Artur Korniłowicz. Implementing More Explicit Definitional Expansions in Mizar (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 37:1-37:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{grabowski_et_al:LIPIcs.ITP.2023.37,
author = {Grabowski, Adam and Korni{\l}owicz, Artur},
title = {{Implementing More Explicit Definitional Expansions in Mizar}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {37:1--37:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.37},
URN = {urn:nbn:de:0030-drops-184121},
doi = {10.4230/LIPIcs.ITP.2023.37},
annote = {Keywords: Mizar, definitions, proof assistants, mechanization of proof}
}
Document
Short Paper
Formalizing Almost Development Closed Critical Pairs (Short Paper)
Abstract
We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.
Cite as
Christina Kohl and Aart Middeldorp. Formalizing Almost Development Closed Critical Pairs (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kohl_et_al:LIPIcs.ITP.2023.38,
author = {Kohl, Christina and Middeldorp, Aart},
title = {{Formalizing Almost Development Closed Critical Pairs}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {38:1--38:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.38},
URN = {urn:nbn:de:0030-drops-184130},
doi = {10.4230/LIPIcs.ITP.2023.38},
annote = {Keywords: Term rewriting, confluence, certification}
}