eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
1
660
10.4230/LIPIcs.ITP.2023
article
LIPIcs, Volume 268, ITP 2023, Complete Volume
Naumowicz, Adam
1
https://orcid.org/0000-0003-4224-9798
Thiemann, René
2
https://orcid.org/0000-0002-0323-8829
University of Białystok, Poland
University of Innsbruck, Austria
LIPIcs, Volume 268, ITP 2023, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023/LIPIcs.ITP.2023.pdf
LIPIcs, Volume 268, ITP 2023, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
0:i
0:x
10.4230/LIPIcs.ITP.2023.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Naumowicz, Adam
1
https://orcid.org/0000-0003-4224-9798
Thiemann, René
2
https://orcid.org/0000-0002-0323-8829
University of Białystok, Poland
University of Innsbruck, Austria
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.0/LIPIcs.ITP.2023.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
1:1
1:2
10.4230/LIPIcs.ITP.2023.1
article
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
Koutsoukou-Argyraki, Angeliki
1
https://orcid.org/0000-0002-8886-5281
University of Cambridge, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.1/LIPIcs.ITP.2023.1.pdf
Additive combinatorics
additive number theory
combinatorial number theory
formalisation of mathematics
interactive theorem proving
proof assistants
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
2:1
2:1
10.4230/LIPIcs.ITP.2023.2
article
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
Krebbers, Robbert
1
https://orcid.org/0000-0002-1185-5237
Radboud University, Nijmegen, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.2/LIPIcs.ITP.2023.2.pdf
Program Verification
Separation Logic
Step-Indexing
Modal Logic
Interactive Theorem Proving
Proof Automation
Iris
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
3:1
3:18
10.4230/LIPIcs.ITP.2023.3
article
A Formal Analysis of RANKING
Abdulaziz, Mohammad
1
2
https://orcid.org/0000-0002-8244-518X
Madlener, Christoph
2
https://orcid.org/0000-0002-9577-0061
King’s College London, UK
Technische Universität München, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.3/LIPIcs.ITP.2023.3.pdf
Matching Theory
Formalized Mathematics
Online Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
4:1
4:17
10.4230/LIPIcs.ITP.2023.4
article
Fast, Verified Computation for Candle
Abrahamsson, Oskar
1
https://orcid.org/0000-0002-4861-2650
Myreen, Magnus O.
1
https://orcid.org/0000-0002-9504-4107
Chalmers University of Technology, Gothenburg, Sweden
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.4/LIPIcs.ITP.2023.4.pdf
Prover soundness
Higher-order logic
Interactive theorem proving
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
5:1
5:21
10.4230/LIPIcs.ITP.2023.5
article
Formalizing Functions as Processes
Accattoli, Beniamino
1
https://orcid.org/0000-0003-4944-9944
Blanc, Horace
2
Sacerdoti Coen, Claudio
3
Inria & LIX, École Poytechnique, Palaiseau, France
Independent researcher, Paris, France
Alma Mater Studiorum - University of Bologna, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.5/LIPIcs.ITP.2023.5.pdf
Lambda calculus
pi calculus
proof assistants
binders
Abella
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
6:1
6:19
10.4230/LIPIcs.ITP.2023.6
article
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic
Angdinata, David Kurniadi
1
https://orcid.org/0000-0003-2096-1864
Xu, Junyan
2
https://orcid.org/0000-0002-3789-2319
London School of Geometry and Number Theory, UK
Cancer Data Science Laboratory, National Cancer Institute, Bethesda, MD, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.6/LIPIcs.ITP.2023.6.pdf
formal math
algebraic geometry
elliptic curve
group law
Lean
mathlib
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
7:1
7:19
10.4230/LIPIcs.ITP.2023.7
article
A Proof-Producing Compiler for Blockchain Applications
Avigad, Jeremy
1
https://orcid.org/0000-0003-1275-315X
Goldberg, Lior
2
Levit, David
2
Seginer, Yoav
3
Titelman, Alon
2
Carnegie Mellon University, Pittsburgh, PA, USA
StarkWare Industries Ltd., Netanya, Israel
Amsterdam, Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.7/LIPIcs.ITP.2023.7.pdf
formal verification
smart contracts
interactive proof systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
8:1
8:18
10.4230/LIPIcs.ITP.2023.8
article
No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
Bosman, Roger
1
https://orcid.org/0000-0002-6693-4653
Karachalias, Georgios
2
Schrijvers, Tom
1
https://orcid.org/0000-0001-8771-5559
KU Leuven, Belgium
Tweag, Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.8/LIPIcs.ITP.2023.8.pdf
type inference
mechanization
let-polymorphism
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
9:1
9:19
10.4230/LIPIcs.ITP.2023.9
article
Automated Theorem Proving for Metamath
Carneiro, Mario
1
https://orcid.org/0000-0002-0470-5249
Brown, Chad E.
2
Urban, Josef
2
Carnegie Mellon University, Pittsburgh, PA, USA
Czech Technical University in Prague, Czech Republic
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.9/LIPIcs.ITP.2023.9.pdf
Metamath
Automated theorem proving
Interactive theorem proving
Formal proof assistants
proof discovery
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
10:1
10:18
10.4230/LIPIcs.ITP.2023.10
article
Reimplementing Mizar in Rust
Carneiro, Mario
1
https://orcid.org/0000-0002-0470-5249
Carnegie Mellon University, Pittsburgh, PA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.10/LIPIcs.ITP.2023.10.pdf
Mizar
proof checker
software
Rust
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
11:1
11:19
10.4230/LIPIcs.ITP.2023.11
article
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
Cruz-Filipe, Luís
1
https://orcid.org/0000-0002-7866-7484
Montesi, Fabrizio
1
https://orcid.org/0000-0003-4666-901X
Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.11/LIPIcs.ITP.2023.11.pdf
choreographic programming
theorem proving
compilation
program repair
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
12:1
12:18
10.4230/LIPIcs.ITP.2023.12
article
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
de Almeida Borges, Ana
1
https://orcid.org/0000-0001-5152-198X
Casanueva Artís, Annalí
2
Falleri, Jean-Rémy
3
https://orcid.org/0000-0002-8284-7218
Gallego Arias, Emilio Jesús
4
https://orcid.org/0000-0002-9299-1192
Martin-Dorel, Érik
5
https://orcid.org/0000-0001-9716-9491
Palmskog, Karl
6
https://orcid.org/0000-0003-0228-1240
Serebrenik, Alexander
7
https://orcid.org/0000-0002-1418-0095
Zimmermann, Théo
8
https://orcid.org/0000-0002-3580-8806
University of Barcelona, Spain
Ifo Institut, München, Germany
Univ. Bordeaux, Bordeaux INP, CNRS, UMR 5800 LaBRI, F-33400 Talence, Institut Universitaire de France, France
Université Paris Cité, CNRS, Inria, IRIF, F-75013, Paris, France
IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, France
KTH Royal Institute of Technology, Stockholm, Sweden
TU Eindhoven, The Netherlands
LTCI, Télécom Paris, Institut Polytechnique de Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.12/LIPIcs.ITP.2023.12.pdf
Coq
Community
Survey
Statistical Analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
13:1
13:18
10.4230/LIPIcs.ITP.2023.13
article
Formalizing Norm Extensions and Applications to Number Theory
de Frutos-Fernández, María Inés
1
2
https://orcid.org/0000-0002-5085-7446
Imperial College London, UK
Universidad Autónoma de Madrid, Spain
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.13/LIPIcs.ITP.2023.13.pdf
formal mathematics
Lean
mathlib
algebraic number theory
p-adic analysis
Galois representations
p-adic Hodge theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
14:1
14:20
10.4230/LIPIcs.ITP.2023.14
article
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure
Dunn, Lawrence
1
https://orcid.org/0000-0001-6808-9441
Tannen, Val
1
https://orcid.org/0009-0008-6847-7274
Zdancewic, Steve
1
https://orcid.org/0000-0002-3516-1512
University of Pennsylvania, Philadelphia, PA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.14/LIPIcs.ITP.2023.14.pdf
Coq
category theory
formal metatheory
raw syntax
locally nameless
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
15:1
15:16
10.4230/LIPIcs.ITP.2023.15
article
Closure Properties of General Grammars – Formally Verified
Dvorak, Martin
1
https://orcid.org/0000-0001-5293-214X
Blanchette, Jasmin
2
https://orcid.org/0000-0002-8367-0936
Institute of Science and Technology Austria, Klosterneuburg, Austria
Ludwig-Maximilians-Universität München, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.15/LIPIcs.ITP.2023.15.pdf
Lean
type-0 grammars
recursively enumerable languages
Kleene star
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
16:1
16:17
10.4230/LIPIcs.ITP.2023.16
article
Formalising Yoneda Ext in Univalent Foundations
Flaten, Jarl G. Taxerås
1
https://orcid.org/0000-0001-6670-6928
University of Western Ontario, London, Ontario, Canada
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.16/LIPIcs.ITP.2023.16.pdf
homotopy type theory
homological algebra
Yoneda Ext
formalisation
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
17:1
17:19
10.4230/LIPIcs.ITP.2023.17
article
LISA - A Modern Proof System
Guilloud, Simon
1
https://orcid.org/0000-0001-8179-7549
Gambhir, Sankalp
1
https://orcid.org/0000-0001-5994-1081
Kunčak, Viktor
1
https://orcid.org/0000-0001-7044-9522
Laboratory for Automated Reasoning and Analysis, EPFL, Lausanne, Switzerland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.17/LIPIcs.ITP.2023.17.pdf
Proof assistant
First Order Logic
Set Theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
18:1
18:18
10.4230/LIPIcs.ITP.2023.18
article
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
Hirata, Michikazu
1
Minamide, Yasuhiko
1
Sato, Tetsuya
1
School of Computing, Tokyo Institute of Technology, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.18/LIPIcs.ITP.2023.18.pdf
Higher-order probabilistic program
s-finite kernel
Quasi-Borel spaces
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
19:1
19:22
10.4230/LIPIcs.ITP.2023.19
article
MizAR 60 for Mizar 50
Jakubův, Jan
1
https://orcid.org/0000-0002-8848-5537
Chvalovský, Karel
1
https://orcid.org/0000-0002-0541-3889
Goertzel, Zarathustra
1
https://orcid.org/0000-0002-8458-2786
Kaliszyk, Cezary
2
3
https://orcid.org/0000-0002-8273-6059
Olšák, Mirek
4
https://orcid.org/0000-0002-9361-1921
Piotrowski, Bartosz
1
https://orcid.org/0000-0002-1699-018X
Schulz, Stephan
5
https://orcid.org/0000-0001-6262-8555
Suda, Martin
1
https://orcid.org/0000-0003-0989-5800
Urban, Josef
1
https://orcid.org/0000-0002-1384-1613
Czech Technical University in Prague, Czech Republic
Universität Innsbruck, Austria
INDRC, Prague, Czech Republic
Institut des Hautes Études Scientifiques, Paris, France
DHBW Stuttgart, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.19/LIPIcs.ITP.2023.19.pdf
Mizar
ENIGMA
Automated Reasoning
Machine Learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
20:1
20:19
10.4230/LIPIcs.ITP.2023.20
article
Constructive Final Semantics of Finite Bags
Joram, Philipp
1
https://orcid.org/0000-0002-0448-7907
Veltri, Niccolò
1
https://orcid.org/0000-0002-7230-3436
Department of Software Science, Tallinn University of Technology, Estonia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.20/LIPIcs.ITP.2023.20.pdf
finite bags
final coalgebra
homotopy type theory
Cubical Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
21:1
21:17
10.4230/LIPIcs.ITP.2023.21
article
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq
Larchey-Wendling, Dominique
1
Monin, Jean-François
2
Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France
Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.21/LIPIcs.ITP.2023.21.pdf
Unbounded linear search
μ-recursive functions
computational contents
Coq
extraction
OCaml
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
22:1
22:17
10.4230/LIPIcs.ITP.2023.22
article
Group Cohomology in the Lean Community Library
Livingston, Amelia
1
King’s College London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.22/LIPIcs.ITP.2023.22.pdf
formal math
Lean
mathlib
group cohomology
homological algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
23:1
23:16
10.4230/LIPIcs.ITP.2023.23
article
A Formalisation of Gallagher’s Ergodic Theorem
Nash, Oliver
1
https://orcid.org/0000-0001-7208-6307
Imperial College London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.23/LIPIcs.ITP.2023.23.pdf
Lean proof assistant
measure theory
metric number theory
ergodicity
Gallagher’s theorem
Duffin-Schaeffer conjecture
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
24:1
24:20
10.4230/LIPIcs.ITP.2023.24
article
An Extensible User Interface for Lean 4
Nawrocki, Wojciech
1
https://orcid.org/0000-0002-8839-0618
Ayers, Edward W.
1
https://orcid.org/0000-0003-1846-1473
Ebner, Gabriel
2
https://orcid.org/0000-0003-4057-9574
Carnegie Mellon University, Pittsburgh, PA, USA
Microsoft Research, Redmond, WA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.24/LIPIcs.ITP.2023.24.pdf
user interfaces
human-computer interaction
Lean
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
25:1
25:19
10.4230/LIPIcs.ITP.2023.25
article
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
Pomeret-Coquot, Pierre
1
https://orcid.org/0000-0003-2243-5913
Fargier, Hélène
2
https://orcid.org/0000-0003-1616-5961
Martin-Dorel, Érik
1
https://orcid.org/0000-0001-9716-9491
IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, France
IRIT, CNRS, Toulouse, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.25/LIPIcs.ITP.2023.25.pdf
Game of Incomplete Information
Belief Function Theory
Coq Proof Assistant
SSReflect Proof Language
MathComp Library
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
26:1
26:20
10.4230/LIPIcs.ITP.2023.26
article
Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
Reichel, Tom
1
Henderson, R. Wesley
2
Touchet, Andrew
2
Gardner, Andrew
2
Ringer, Talia
1
University of Illinois Urbana-Champaign, IL, USA
Radiance Technologies, Inc., Ruston, LA, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.26/LIPIcs.ITP.2023.26.pdf
proof repair
datasets
benchmarks
machine learning
formal proof
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
27:1
27:18
10.4230/LIPIcs.ITP.2023.27
article
POSIX Lexing with Bitcoded Derivatives
Tan, Chengsong
1
Urban, Christian
2
Imperial College London, UK
King’s College London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.27/LIPIcs.ITP.2023.27.pdf
POSIX matching and lexing
derivatives of regular expressions
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
28:1
28:19
10.4230/LIPIcs.ITP.2023.28
article
A Sound and Complete Projection for Global Types
Tirore, Dawit
1
Bengtson, Jesper
1
Carbone, Marco
1
IT University of Copenhagen, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.28/LIPIcs.ITP.2023.28.pdf
Session types
Mechanisation
Projection
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
29:1
29:18
10.4230/LIPIcs.ITP.2023.29
article
Real-Time Double-Ended Queue Verified (Proof Pearl)
Toth, Balazs
1
Nipkow, Tobias
1
https://orcid.org/0000-0003-0730-515X
Department of Computer Science, Technische Univerität München, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.29/LIPIcs.ITP.2023.29.pdf
Double-ended queue
data structures
verification
Isabelle
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
30:1
30:20
10.4230/LIPIcs.ITP.2023.30
article
Certifying Higher-Order Polynomial Interpretations
van der Weide, Niels
1
https://orcid.org/0000-0003-1146-4161
Vale, Deivid
1
https://orcid.org/0000-0003-1350-3478
Kop, Cynthia
1
https://orcid.org/0000-0002-6337-2544
Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.30/LIPIcs.ITP.2023.30.pdf
higher-order rewriting
Coq
termination
formalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
31:1
31:19
10.4230/LIPIcs.ITP.2023.31
article
Slice Nondeterminism
Voorneveld, Niels F. W.
1
https://orcid.org/0000-0001-6650-3493
Tallinn University of Technology, Estonia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.31/LIPIcs.ITP.2023.31.pdf
Category theory
Agda
Slice category
Nondeterministic functions
Powerset
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
32:1
32:20
10.4230/LIPIcs.ITP.2023.32
article
Foundational Verification of Stateful P4 Packet Processing
Wang, Qinshi
1
https://orcid.org/0000-0002-6486-3409
Pan, Mengying
1
https://orcid.org/0000-0001-8970-9697
Wang, Shengyi
1
https://orcid.org/0000-0002-2286-8703
Doenges, Ryan
2
https://orcid.org/0000-0002-6899-4529
Beringer, Lennart
1
https://orcid.org/0000-0002-1570-3492
Appel, Andrew W.
1
https://orcid.org/0000-0001-6009-0325
Princeton University, NJ, USA
Cornell University, Ithaca, NY, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.32/LIPIcs.ITP.2023.32.pdf
Software Defined Networking
Verifiable P4
Stateful data plane programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
33:1
33:18
10.4230/LIPIcs.ITP.2023.33
article
Dependently Sorted Theorem Proving for Mathematical Foundations
Xu, Yiming
1
https://orcid.org/0009-0002-4006-0983
Norrish, Michael
1
https://orcid.org/0000-0003-1163-8467
Australian National University, Canberra, Australia
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_{ω+ω}.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.33/LIPIcs.ITP.2023.33.pdf
first order logic
sorts
structural set theory
mechanised mathematics
foundation of mathematics
category theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
34:1
34:13
10.4230/LIPIcs.ITP.2023.34
article
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)
Yamada, Akihisa
1
https://orcid.org/0000-0001-8872-2240
Dubut, Jérémy
1
https://orcid.org/0000-0002-2640-3065
National Institute of Advanced Industrial Science and Technology, Tokyo, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.34/LIPIcs.ITP.2023.34.pdf
Directed Sets
Completeness
Scott Continuous Functions
Ordinals
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
35:1
35:17
10.4230/LIPIcs.ITP.2023.35
article
Formalising the Proj Construction in Lean
Zhang, Jujian
1
https://orcid.org/0000-0001-7340-2703
Department of Mathematics, Imperial College London, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.35/LIPIcs.ITP.2023.35.pdf
Lean
formalisation
algebraic geometry
scheme
Proj construction
projective geometry
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
36:1
36:8
10.4230/LIPIcs.ITP.2023.36
article
Fermat’s Last Theorem for Regular Primes (Short Paper)
Best, Alex J.
1
https://orcid.org/0000-0002-5741-674X
Birkbeck, Christopher
2
https://orcid.org/0000-0002-7546-9028
Brasca, Riccardo
3
https://orcid.org/0000-0002-0491-7241
Rodriguez Boidi, Eric
1
https://orcid.org/0000-0002-0507-627X
King’s College London, UK
University of East Anglia, Norwich, UK
Université Paris Cité, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.36/LIPIcs.ITP.2023.36.pdf
Fermat’s Last Theorem
Cyclotomic fields
Interactive theorem proving
Lean
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
37:1
37:8
10.4230/LIPIcs.ITP.2023.37
article
Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
Grabowski, Adam
1
https://orcid.org/0000-0001-5026-3990
Korniłowicz, Artur
1
https://orcid.org/0000-0002-4565-9082
Institute of Computer Science, University of Białystok, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.37/LIPIcs.ITP.2023.37.pdf
Mizar
definitions
proof assistants
mechanization of proof
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2023-07-26
268
38:1
38:8
10.4230/LIPIcs.ITP.2023.38
article
Formalizing Almost Development Closed Critical Pairs (Short Paper)
Kohl, Christina
1
https://orcid.org/0000-0002-8470-2485
Middeldorp, Aart
1
https://orcid.org/0000-0001-7366-8464
Universität Innsbruck, Austria
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.38/LIPIcs.ITP.2023.38.pdf
Term rewriting
confluence
certification