eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
0
0
10.4230/LIPIcs.ITP.2019
article
LIPIcs, Volume 141, ITP'19, Complete Volume
Harrison, John
1
O'Leary, John
2
Tolmach, Andrew
3
Amazon AWS, Portland, OR, USA
Intel Corporation
Portland State University, Portland, OR, USA
LIPIcs, Volume 141, ITP'19, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019/LIPIcs.ITP.2019.pdf
Theory of computation, Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
0:i
0:xiv
10.4230/LIPIcs.ITP.2019.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Harrison, John
1
O'Leary, John
2
Tolmach, Andrew
3
Amazon AWS, Portland, OR, USA
Intel Corporation
Portland State University, Portland, OR, USA
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.0/LIPIcs.ITP.2019.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
2019-09-05
141
1:1
1:1
10.4230/LIPIcs.ITP.2019.1
article
A Million Lines of Proof About a Moving Target (Invited Talk)
Andronick, June
1
2
CSIRO's Data61, Sydney, Australia
UNSW, Sydney, Australia
In the last ten years, we have been porting, maintaining, and evolving the world’s largest proof base, the formal proof in Isabelle/HOL of the seL4 microkernel. But actually, there is no such thing as "the seL4 proof"; there are a number of proofs (functional correctness, binary translation validation, integrity and confidentiality proofs, etc) about a number of instances of seL4 (depending on the hardware platform it runs on, the features it includes, the extensions it supports). We will give an overview of the current state of these proofs, and, importantly, the challenges we face in keeping to maintain, evolve and extend them, and the processes we have put in place to manage their dependence on the evolving implementation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.1/LIPIcs.ITP.2019.1.pdf
Proof maintentance
proof evolution
seL4
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
2:1
2:1
10.4230/LIPIcs.ITP.2019.2
article
What Makes a Mathematician Tick? (Invited Talk)
Buzzard, Kevin
1
Imperial College, London, U.K.
Formalised mathematics has a serious image problem in mathematics departments. Mathematicians working in "mainstream" areas such as modern algebra, analysis, geometry etc have absolutely no desire to work formally, it slows them down and they cannot see the point. The mathematical community has its own methods for deciding whether a proof (in pdf format) is correct or not; these methods rely on the views of a cabal of experts - our high priests. Our proof of the odd order theorem is "John Thompson got a Fields Medal for the work". This proof is of a rather different nature to the formalised proof of Gonthier et al. Our methods are arcane and mysterious; there is also ample evidence that they are, in general, extremely accurate when it comes to the important stuff.
I will talk about my attempts, as a "mainstream mathematician", to introduce formalised mathematics to my community.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.2/LIPIcs.ITP.2019.2.pdf
Formalization of mathematics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
3:1
3:1
10.4230/LIPIcs.ITP.2019.3
article
An Increasing Need for Formality (Invited Talk)
Dixon, Martin
1
Intel Corp., Hillsboro, Oregon, USA
The talk will touch on a number of practical opportunities for formal modeling and methods that Intel sees in HW security research including: instruction sets; the proliferation of programmable agents within SoC’s; and negative space testing.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.3/LIPIcs.ITP.2019.3.pdf
Hardware security
formal modeling
instruction sets
SoC’s
negative space testing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
4:1
4:19
10.4230/LIPIcs.ITP.2019.4
article
A Verified Compositional Algorithm for AI Planning
Abdulaziz, Mohammad
1
https://orcid.org/0000-0002-8244-518X
Gretton, Charles
2
https://orcid.org/0000-0001-9803-0168
Norrish, Michael
3
2
https://orcid.org/0000-0003-1163-8467
Technical University of Munich, Germany
Australian National University, Canberra, Australia
Data61, CSIRO, Canberra, Australia
We report on our HOL4 verification of an AI planning algorithm. The algorithm is compositional in the following sense: a planning problem is divided into multiple smaller abstractions, then each of the abstractions is solved, and finally the abstractions' solutions are composed into a solution for the given problem. Formalising the algorithm, which was already quite well understood, revealed nuances in its operation which could lead to computing buggy plans. The formalisation also revealed that the algorithm can be presented more generally, and can be applied to systems with infinite states and actions, instead of only finite ones.
Our formalisation extends an earlier model for slightly simpler transition systems, and demonstrates another step towards formal treatments of more and more of the algorithms and reasoning used in AI planning, as well as model checking.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.4/LIPIcs.ITP.2019.4.pdf
AI Planning
Compositional Algorithms
Algorithm Verification
Transition Systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
5:1
5:19
10.4230/LIPIcs.ITP.2019.5
article
Proving Tree Algorithms for Succinct Data Structures
Affeldt, Reynald
1
https://orcid.org/0000-0002-2327-953X
Garrigue, Jacques
2
https://orcid.org/0000-0001-8056-5519
Qi, Xuanrui
3
https://orcid.org/0000-0002-2032-1552
Tanaka, Kazunari
2
https://orcid.org/0000-0001-8460-7763
National Institute of Advanced Industrial Science and Technology, Tsukuba, Japan
Graduate School of Mathematics, Nagoya University, Japan
Department of Computer Science, Tufts University, Medford, MA, United States
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different tree-based succinct representations and their accompanying algorithms. One is the Level-Order Unary Degree Sequence, which encodes the structure of a tree in breadth-first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary balanced trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient insertion and deletion. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.5/LIPIcs.ITP.2019.5.pdf
Coq
small-scale reflection
succinct data structures
LOUDS
bit vectors
self balancing trees
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
6:1
6:19
10.4230/LIPIcs.ITP.2019.6
article
Data Types as Quotients of Polynomial Functors
Avigad, Jeremy
1
https://orcid.org/0000-0003-1275-315X
Carneiro, Mario
1
https://orcid.org/0000-0002-0470-5249
Hudon, Simon
1
Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.6/LIPIcs.ITP.2019.6.pdf
data types
polynomial functors
inductive types
coinductive types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
7:1
7:20
10.4230/LIPIcs.ITP.2019.7
article
Primitive Floats in Coq
Bertholon, Guillaume
1
https://orcid.org/0000-0001-7000-382X
Martin-Dorel, Érik
2
https://orcid.org/0000-0001-9716-9491
Roux, Pierre
3
https://orcid.org/0000-0003-2910-4738
École Normale Supérieure, Paris, France
Lab. IRIT, University of Toulouse, CNRS, France
ONERA, Toulouse, France
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors.
Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers.
A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.7/LIPIcs.ITP.2019.7.pdf
Coq formal proofs
floating-point arithmetic
reflexive tactics
Cholesky decomposition
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
8:1
8:19
10.4230/LIPIcs.ITP.2019.8
article
A Certificate-Based Approach to Formally Verified Approximations
Bréhard, Florent
1
2
Mahboubi, Assia
3
Pous, Damien
4
Plume and AriC teams, LIP, ENS de Lyon, Université de Lyon, Lyon, France
MAC team, LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France
Gallinette team, LS2N, INRIA, Université de Nantes, Nantes, France
Plume team, LIP, CNRS, ENS de Lyon, Université de Lyon, Lyon, France
We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.8/LIPIcs.ITP.2019.8.pdf
approximation theory
Chebyshev polynomials
Banach fixed-point theorem
interval arithmetic
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
9:1
9:16
10.4230/LIPIcs.ITP.2019.9
article
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof
Brown, Chad E.
1
Kaliszyk, Cezary
2
3
https://orcid.org/0000-0002-8273-6059
Pąk, Karol
4
https://orcid.org/0000-0002-7099-1669
Czech Technical University in Prague, Czech Republic
University of Innsbruck, Austria
University of Warsaw, Poland
University of Białystok, Poland
We formally introduce a foundation for computer verified proofs based on higher-order Tarski-Grothendieck set theory. We show that this theory has a model if a 2-inaccessible cardinal exists. This assumption is the same as the one needed for a model of plain Tarski-Grothendieck set theory. The foundation allows the co-existence of proofs based on two major competing foundations for formal proofs: higher-order logic and TG set theory. We align two co-existing Isabelle libraries, Isabelle/HOL and Isabelle/Mizar, in a single foundation in the Isabelle logical framework. We do this by defining isomorphisms between the basic concepts, including integers, functions, lists, and algebraic structures that preserve the important operations. With this we can transfer theorems proved in higher-order logic to TG set theory and vice versa. We practically show this by formally transferring Lagrange’s four-square theorem, Fermat 3-4, and other theorems between the foundations in the Isabelle framework.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.9/LIPIcs.ITP.2019.9.pdf
model
higher-order
Tarski Grothendieck
proof foundation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
10:1
10:18
10.4230/LIPIcs.ITP.2019.10
article
Generic Authenticated Data Structures, Formally
Brun, Matthias
1
Traytel, Dmitriy
2
https://orcid.org/0000-0001-7982-2768
Department of Computer Science, ETH Zürich, Switzerland
Institute of Information Security, Department of Computer Science, ETH Zürich, Switzerland
Authenticated data structures are a technique for outsourcing data storage and maintenance to an untrusted server. The server is required to produce an efficiently checkable and cryptographically secure proof that it carried out precisely the requested computation. Recently, Miller et al. [https://doi.org/10.1145/2535838.2535851] demonstrated how to support a wide range of such data structures by integrating an authentication construct as a first class citizen in a functional programming language. In this paper, we put this work to the test of formalization in the Isabelle proof assistant. With Isabelle’s help, we uncover and repair several mistakes and modify the small-step semantics to perform call-by-value evaluation rather than requiring terms to be in administrative normal form.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.10/LIPIcs.ITP.2019.10.pdf
Authenticated Data Structures
Verifiable Computation
Isabelle/HOL
Nominal Isabelle
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
11:1
11:19
10.4230/LIPIcs.ITP.2019.11
article
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
Brunner, Julian
1
https://orcid.org/0000-0001-8922-6097
Seidl, Benedikt
1
https://orcid.org/0000-0002-9913-8709
Sickert, Salomon
1
https://orcid.org/0000-0002-0280-8981
Technische Universität München, Germany
We present a formalisation of the unified translation approach from linear temporal logic (LTL) to omega-automata from [Javier Esparza et al., 2018]. This approach decomposes LTL formulas into "simple" languages and allows a clear separation of concerns: first, we formalise the purely logical result yielding this decomposition; second, we develop a generic, executable, and expressive automata library providing necessary operations on automata to re-combine the "simple" languages; third, we instantiate this generic theory to obtain a construction for deterministic Rabin automata (DRA). We extract from this particular instantiation an executable tool translating LTL to DRAs. To the best of our knowledge this is the first verified translation of LTL to DRAs that is proven to be double-exponential in the worst case which asymptotically matches the known lower bound.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.11/LIPIcs.ITP.2019.11.pdf
Automata Theory
Automata over Infinite Words
Deterministic Automata
Linear Temporal Logic
Model Checking
Verified Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
12:1
12:17
10.4230/LIPIcs.ITP.2019.12
article
Formalizing Computability Theory via Partial Recursive Functions
Carneiro, Mario
1
https://orcid.org/0000-0002-0470-5249
Carnegie Mellon University, Pittsburgh, PA, USA
We present an extension to the mathlib library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply Gödel numberings where needed and encapsulate the encoding details.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.12/LIPIcs.ITP.2019.12.pdf
Lean
computability
halting problem
primitive recursion
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
13:1
13:19
10.4230/LIPIcs.ITP.2019.13
article
Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
Chen, Ran
1
Cohen, Cyril
2
Lévy, Jean-Jacques
3
Merz, Stephan
4
Théry, Laurent
2
Institute of Software of the Chinese Academy of Sciences, Beijing, China
Université Côte d'Azur, Inria, Sophia Antipolis, France
Irif & Inria, Paris, France
Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.13/LIPIcs.ITP.2019.13.pdf
Mathematical logic
Formal proof
Graph algorithm
Program verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
14:1
14:18
10.4230/LIPIcs.ITP.2019.14
article
First-Order Guarded Coinduction in Coq
Czajka, Łukasz
1
https://orcid.org/0000-0001-8083-4280
Faculty of Informatics, TU Dortmund University, Germany
We introduce two coinduction principles and two proof translations which, under certain conditions, map coinductive proofs that use our principles to guarded Coq proofs. The first principle provides an "operational" description of a proof by coinduction, which is easy to reason with informally. The second principle extends the first one to allow for direct proofs by coinduction of statements with existential quantifiers and multiple coinductive predicates in the conclusion. The principles automatically enforce the correct use of the coinductive hypothesis. We implemented the principles and the proof translations in a Coq plugin.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.14/LIPIcs.ITP.2019.14.pdf
coinduction
Coq
guardedness
corecursion
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
15:1
15:19
10.4230/LIPIcs.ITP.2019.15
article
Formalizing the Solution to the Cap Set Problem
Dahmen, Sander R.
1
https://orcid.org/0000-0002-0014-0789
Hölzl, Johannes
2
https://orcid.org/0000-0003-0869-9250
Lewis, Robert Y.
2
https://orcid.org/0000-0002-5266-1121
Department of Mathematics, Vrije Universiteit Amsterdam, The Netherlands
Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F^n_q with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case q = 3, where it is commonly known as the cap set problem. Ellenberg and Gijswijt’s proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in F^n_q and concrete values for the case q = 3. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.15/LIPIcs.ITP.2019.15.pdf
formal proof
combinatorics
cap set problem
Lean
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
16:1
16:19
10.4230/LIPIcs.ITP.2019.16
article
Nine Chapters of Analytic Number Theory in Isabelle/HOL
Eberl, Manuel
1
https://orcid.org/0000-0002-4263-6571
Technical University of Munich, Boltzmannstraße 3, Garching bei München, Germany
In this paper, I present a formalisation of a large portion of Apostol’s Introduction to Analytic Number Theory in Isabelle/HOL. Of the 14 chapters in the book, the content of 9 has been mostly formalised, while the content of 3 others was already mostly available in Isabelle before.
The most interesting results that were formalised are:
- The Riemann and Hurwitz zeta functions and the Dirichlet L functions
- Dirichlet’s theorem on primes in arithmetic progressions
- An analytic proof of the Prime Number Theorem
- The asymptotics of arithmetical functions such as the prime omega function, the divisor count sigma_0(n), and Euler’s totient function phi(n)
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.16/LIPIcs.ITP.2019.16.pdf
Isabelle
theorem proving
analytic number theory
number theory
arithmetical function
Dirichlet series
prime number theorem
Dirichlet’s theorem
zeta function
L functions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
17:1
17:19
10.4230/LIPIcs.ITP.2019.17
article
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus
Forster, Yannick
1
Kunze, Fabian
1
Saarland University, Saarland Informatics Campus (SIC), Saarbrücken, Germany
We provide a plugin extracting Coq functions of simple polymorphic types to the (untyped) call-by-value lambda calculus L. The plugin is implemented in the MetaCoq framework and entirely written in Coq. We provide Ltac tactics to automatically verify the extracted terms w.r.t a logical relation connecting Coq functions with correct extractions and time bounds, essentially performing a certifying translation and running time validation. We provide three case studies: A universal L-term obtained as extraction from the Coq definition of a step-indexed self-interpreter for L, a many-reduction from solvability of Diophantine equations to the halting problem of L, and a polynomial-time simulation of Turing machines in L.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.17/LIPIcs.ITP.2019.17.pdf
call-by-value
lambda calculus
Coq
constructive type theory
extraction
computability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
18:1
18:20
10.4230/LIPIcs.ITP.2019.18
article
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm
Guéneau, Armaël
1
Jourdan, Jacques-Henri
2
Charguéraud, Arthur
3
Pottier, François
1
Inria, Paris, France
CNRS, LRI, Univ. Paris Sud, Université Paris Saclay, France
Inria & Université de Strasbourg, CNRS, ICube, Strasbourg, France
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.18/LIPIcs.ITP.2019.18.pdf
interactive deductive program verification
complexity analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
19:1
19:19
10.4230/LIPIcs.ITP.2019.19
article
A Formalization of Forcing and the Unprovability of the Continuum Hypothesis
Han, Jesse Michael
1
van Doorn, Floris
1
Department of Mathematics, University of Pittsburgh, PA, USA
We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space 2^{omega_2 x omega} and formally verify the failure of the continuum hypothesis in the resulting model.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.19/LIPIcs.ITP.2019.19.pdf
Interactive theorem proving
formal verification
set theory
forcing
independence proofs
continuum hypothesis
Boolean-valued models
Lean
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
20:1
20:18
10.4230/LIPIcs.ITP.2019.20
article
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL
Haslbeck, Maximilian P. L.
1
https://orcid.org/0000-0003-4306-869X
Lammich, Peter
2
https://orcid.org/0000-0003-3576-0504
Technische Universität München, Germany
The University of Manchester, England
Separation Logic with Time Credits is a well established method to formally verify the correctness and run-time of algorithms, which has been applied to various medium-sized use-cases. Refinement is a technique in program verification that makes software projects of larger scale manageable.
Combining these two techniques for the first time, we present a methodology for verifying the functional correctness and the run-time analysis of algorithms in a modular way. We use it to verify Kruskal’s minimum spanning tree algorithm and the Edmonds - Karp algorithm for network flow.
An adaptation of the Isabelle Refinement Framework [Lammich and Tuerk, 2012] enables us to specify the functional result and the run-time behaviour of abstract algorithms which can be refined to more concrete algorithms. From these, executable imperative code can be synthesized by an extension of the Sepref tool [Lammich, 2015], preserving correctness and the run-time bounds of the abstract algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.20/LIPIcs.ITP.2019.20.pdf
Isabelle
Time Complexity Analysis
Separation Logic
Program Verification
Refinement
Run Time
Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
21:1
21:18
10.4230/LIPIcs.ITP.2019.21
article
Virtualization of HOL4 in Isabelle
Immler, Fabian
1
https://orcid.org/0000-0002-5468-1513
Rädle, Jonas
2
https://orcid.org/0000-0002-7714-0218
Wenzel, Makarius
3
School of Computer Science, Carnegie Mellon University, USA
Fakultät für Informatik, Technische Universität München, Germany
Augsburg, Germany
We present a novel approach to combine the HOL4 and Isabelle theorem provers: both are implemented in SML and based on distinctive variants of HOL. The design of HOL4 allows to replace its inference kernel modules, and the system infrastructure of Isabelle allows to embed other applications of SML. That is the starting point to provide a virtual instance of HOL4 in the same run-time environment as Isabelle. Moreover, with an implementation of a virtual HOL4 kernel that operates on Isabelle/HOL terms and theorems, we can load substantial HOL4 libraries to make them Isabelle theories, but still disconnected from existing Isabelle content. Finally, we introduce a methodology based on the transfer package of Isabelle to connect the imported HOL4 material to that of Isabelle/HOL.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.21/LIPIcs.ITP.2019.21.pdf
Virtualization
HOL4
Isabelle
Isabelle/HOL
Isabelle/ML
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
22:1
22:19
10.4230/LIPIcs.ITP.2019.22
article
Generating Verified LLVM from Isabelle/HOL
Lammich, Peter
1
The University of Manchester, UK
We present a framework to generate verified LLVM programs from Isabelle/HOL. It is based on a code generator that generates LLVM text from a simplified fragment of LLVM, shallowly embedded into Isabelle/HOL. On top, we have developed a separation logic, a verification condition generator, and an LLVM backend to the Isabelle Refinement Framework.
As case studies, we have produced verified LLVM implementations of binary search and the Knuth-Morris-Pratt string search algorithm. These are one order of magnitude faster than the Standard-ML implementations produced with the original Refinement Framework, and on par with unverified C implementations. Adoption of the original correctness proofs to the new LLVM backend was straightforward.
The trusted code base of our approach is the shallow embedding of the LLVM fragment and the code generator, which is a pretty printer combined with some straightforward compilation steps.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.22/LIPIcs.ITP.2019.22.pdf
Isabelle/HOL
LLVM
Separation Logic
Verification Condition Generator
Code Generation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
23:1
23:18
10.4230/LIPIcs.ITP.2019.23
article
Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra
Lammich, Peter
1
https://orcid.org/0000-0003-3576-0504
Nipkow, Tobias
2
https://orcid.org/0000-0003-0730-515X
The University of Manchester, UK
Technical University Munich, Germany
The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. As two applications of this data structure we verify purely functional, simple and efficient implementations of Prim’s and Dijkstra’s algorithms. This constitutes the first verification of an executable and even efficient version of Prim’s algorithm.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.23/LIPIcs.ITP.2019.23.pdf
Priority queue
Dijkstra’s algorithm
Prim’s algorithm
verification
Isabelle
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
24:1
24:18
10.4230/LIPIcs.ITP.2019.24
article
A Verified LL(1) Parser Generator
Lasser, Sam
1
Casinghino, Chris
2
Fisher, Kathleen
1
Roux, Cody
2
Tufts University, Medford, MA, USA
Draper, Cambridge, MA, USA
An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.24/LIPIcs.ITP.2019.24.pdf
interactive theorem proving
top-down parsing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
25:1
25:18
10.4230/LIPIcs.ITP.2019.25
article
Binary-Compatible Verification of Filesystems with ACL2
Mehta, Mihir Parang
1
Cook, William R.
1
University of Texas at Austin, USA
Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level.
This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.25/LIPIcs.ITP.2019.25.pdf
interactive theorem proving
filesystems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
26:1
26:19
10.4230/LIPIcs.ITP.2019.26
article
Ornaments for Proof Reuse in Coq
Ringer, Talia
1
Yazdani, Nathaniel
1
Leo, John
2
Grossman, Dan
1
University of Washington, USA
Halfaya Research, USA
Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.26/LIPIcs.ITP.2019.26.pdf
ornaments
proof reuse
proof automation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
27:1
27:19
10.4230/LIPIcs.ITP.2019.27
article
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security
Sison, Robert
1
2
https://orcid.org/0000-0003-0313-9764
Murray, Toby
3
Data61, CSIRO, Australia
UNSW Sydney, Australia
University of Melbourne, Australia
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency.
Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations.
In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.27/LIPIcs.ITP.2019.27.pdf
Secure compilation
Information flow security
Concurrency
Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
28:1
28:21
10.4230/LIPIcs.ITP.2019.28
article
Quantitative Continuity and Computable Analysis in Coq
Steinberg, Florian
1
Théry, Laurent
2
Thies, Holger
3
INRIA Saclay, France
INRIA Sophia-Antipolis, France
Kyushu University, Japan
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric.
The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.28/LIPIcs.ITP.2019.28.pdf
computable analysis
Coq
contionuous functionals
discontinuity
closed choice on the naturals
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
29:1
29:18
10.4230/LIPIcs.ITP.2019.29
article
Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq
Tassi, Enrico
1
Université côte d'Azur - Inria, France
We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations in Coq. Programs and proofs are derived compositionally, reusing code and proofs derived previously.
The key steps are two. First, we design appropriate induction principles for data types defined using parametric containers. Second, we develop a technique to work around the modularity limitations imposed by the purely syntactic termination check Coq performs on recursive proofs. The unary parametricity translation of inductive data types turns out to be the key to both steps.
Last but not least, we provide an implementation of the procedure for the Coq proof assistant based on the Elpi [Dunchev et al., 2015] extension language.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.29/LIPIcs.ITP.2019.29.pdf
Coq
Containers
Induction
Equality test
Parametricity translation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
30:1
30:16
10.4230/LIPIcs.ITP.2019.30
article
Complete Non-Orders and Fixed Points
Yamada, Akihisa
1
https://orcid.org/0000-0001-8872-2240
Dubut, Jérémy
1
2
National Institute of Informatics, Tokyo, Japan
Japanese-French Laboratory for Informatics, Tokyo, Japan
In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.30/LIPIcs.ITP.2019.30.pdf
Order Theory
Lattice Theory
Fixed-Points
Isabelle/HOL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
31:1
31:19
10.4230/LIPIcs.ITP.2019.31
article
Verified Decision Procedures for Modal Logics
Wu, Minchao
1
https://orcid.org/0000-0001-7651-7944
Goré, Rajeev
1
Research School of Computer Science, Australian National University, Australia
We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.31/LIPIcs.ITP.2019.31.pdf
Formal Methods
Interactive Theorem Proving
Modal Logic
Lean
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
32:1
32:19
10.4230/LIPIcs.ITP.2019.32
article
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs
Åman Pohjola, Johannes
1
Rostedt, Henrik
2
Myreen, Magnus O.
2
Data61/CSIRO, Sydney, Australia, University of New South Wales, Sydney, Australia
Chalmers University of Technology, Gothenburg, Sweden
There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.32/LIPIcs.ITP.2019.32.pdf
Program verification
non-termination
liveness
Hoare logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
33:1
33:7
10.4230/LIPIcs.ITP.2019.33
article
The DPRM Theorem in Isabelle (Short Paper)
Bayer, Jonas
1
David, Marco
2
Pal, Abhik
2
Stock, Benedikt
2
Schleicher, Dierk
3
Freie Universität Berlin, Arnimallee 2, 14195 Berlin, Germany
Jacobs University Bremen, Campus Ring 1, 28759 Bremen, Germany
Technische Universität Berlin, Germany
Hilbert’s 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich’s proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.33/LIPIcs.ITP.2019.33.pdf
DPRM theorem
Hilbert’s tenth problem
Diophantine predicates
Register machines
Recursively enumerable sets
Isabelle
Formal verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
34:1
34:8
10.4230/LIPIcs.ITP.2019.34
article
Hammering Mizar by Learning Clause Guidance (Short Paper)
Jakubův, Jan
1
Urban, Josef
1
Czech Technical University in Prague, Czech Republic
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.34/LIPIcs.ITP.2019.34.pdf
Proof automation
ITP hammers
Automated theorem proving
Machine learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
35:1
35:7
10.4230/LIPIcs.ITP.2019.35
article
Declarative Proof Translation (Short Paper)
Kaliszyk, Cezary
1
2
https://orcid.org/0000-0002-8273-6059
Pąk, Karol
3
https://orcid.org/0000-0002-7099-1669
University of Innsbruck, Austria
University of Warsaw, Poland
University of Białystok, Poland
Declarative proof styles of different proof assistants include a number of incompatible features. In this paper we discuss and classify the differences between them and propose efficient algorithms for declarative proof outline translation. We demonstrate the practicality of our algorithms by automatically translating the proof outlines in 200 articles from the Mizar Mathematical Library to the Isabelle/Isar proof style. This generates the corresponding theories with 15301 proof outlines accepted by the Isabelle proof checker. The goal of our translation is to produce a declarative proof in the target system that is both accepted and short and therefore readable. For this three kinds of adaptations are required. First, the proof structure often needs to be rebuilt to capture the extensions of the natural deduction rules supported by the systems. Second, the references to previous items and their labels need to be matched and aligned. Finally, adaptations in the annotations of individual proof step may be necessary.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.35/LIPIcs.ITP.2019.35.pdf
Declarative Proof
Translation
Isabelle/Isar
Mizar
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-09-05
141
36:1
36:7
10.4230/LIPIcs.ITP.2019.36
article
Formalization of the Domination Chain with Weighted Parameters (Short Paper)
Severín, Daniel E.
1
2
https://orcid.org/0000-0003-2391-3489
Depto. de Matemática, Universidad Nacional de Rosario, Argentina
CONICET, Argentina
The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters of graph theory: for a given graph G, ir(G) <= gamma(G) <= iota(G) <= alpha(G) <= Gamma(G) <= IR(G). These parameters return the maximum/minimum cardinality of a set satisfying some property. However, they can be generalized for graphs with weighted vertices where the objective is to maximize/minimize the sum of weights of a set satisfying the same property, and the domination chain still holds for them. In this work, the definition of these parameters as well as the chain is formalized in Coq/Ssreflect.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.36/LIPIcs.ITP.2019.36.pdf
Domination Chain
Coq
Formalization of Mathematics