We provide a framework for automatically deriving instances for generic type classes. Our approach is inspired by Haskell's generic-deriving package and Scala's shapeless library. In addition to generating the code for type class functions, we also attempt to automatically prove type class laws for these instances. As of now, however, some manual proofs are still required for recursive datatypes.
Note: There are already articles in the AFP that provide automatic instantiation for a number of classes. Concretely, Deriving allows the automatic instantiation of comparators, linear orders, equality, and hashing. Show instantiates a Haskell-style show class.
Our approach works for arbitrary classes (with some Isabelle/HOL overhead for each class), but a smaller set of datatypes.
[Partial_Order_Reduction] title = Partial Order Reduction author = Julian BrunnerThis article gives the basic theory of Pell's equation x2 = 1 + D y2, where D ∈ ℕ is a parameter and x, y are integer variables.
The main result that is proven is the following: If D is not a perfect square, then there exists a fundamental solution (x0, y0) that is not the trivial solution (1, 0) and which generates all other solutions (x, y) in the sense that there exists some n ∈ ℕ such that |x| + |y| √D = (x0 + y0 √D)n. This also implies that the set of solutions is infinite, and it gives us an explicit and executable characterisation of all the solutions.
Based on this, simple executable algorithms for computing the fundamental solution and the infinite sequence of all non-negative solutions are also provided.
[Sophomores_Dream] title = The Sophomore's Dream author = Manuel EberlThis article provides a brief formalisation of the two equations known as the Sophomore's Dream, first discovered by Johann Bernoulli in 1697:
\[\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n} \quad\text{and}\quad \int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}\] [WebAssembly] title = WebAssembly author = Conrad WattMinkowski's theorem relates a subset of ℝn, the Lebesgue measure, and the integer lattice ℤn: It states that any convex subset of ℝn with volume greater than 2n contains at least one lattice point from ℤn\{0}, i. e. a non-zero point with integer coefficients.
A related theorem which directly implies this is Blichfeldt's theorem, which states that any subset of ℝn with a volume greater than 1 contains two different points whose difference vector has integer components.
The entry contains a proof of both theorems.
[Name_Carrying_Type_Inference] title = Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus author = Michael RawsonIn this AFP entry, we show how to specify game-based cryptographic security notions and formally prove secure several cryptographic constructions from the literature using the CryptHOL framework. Among others, we formalise the notions of a random oracle, a pseudo-random function, an unpredictable function, and of encryption schemes that are indistinguishable under chosen plaintext and/or ciphertext attacks. We prove the random-permutation/random-function switching lemma, security of the Elgamal and hashed Elgamal public-key encryption scheme and correctness and security of several constructions with pseudo-random functions.
Our proofs follow the game-hopping style advocated by Shoup and Bellare and Rogaway, from which most of the examples have been taken. We generalise some of their results such that they can be reused in other proofs. Thanks to CryptHOL's integration with Isabelle's parametricity infrastructure, many simple hops are easily justified using the theory of representation independence.
extra-history = Change history: [2018-09-28]: added the CryptHOL tutorial for game-based cryptography (revision 489a395764ae) [Multi_Party_Computation] title = Multi-Party Computation author = David AspinallCryptHOL provides a framework for formalising cryptographic arguments in Isabelle/HOL. It shallowly embeds a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. All operators are defined in the new semantic domain of generative probabilistic values, a codatatype. We derive proof rules for the operators and establish a connection with the theory of relational parametricity. Thus, the resuting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable.
The framework is used in the accompanying AFP entry "Game-based Cryptography in HOL". There, we show-case our framework by formalizing different game-based proofs from the literature. This formalisation continues the work described in the author's ESOP 2016 paper.
[Constructive_Cryptography] title = Constructive Cryptography in HOL author = Andreas LochbihlerThis article contains a formal proof of the well-known fact that number of comparisons that a comparison-based sorting algorithm needs to perform to sort a list of length n is at least log2 (n!) in the worst case, i. e. Ω(n log n).
For this purpose, a shallow embedding for comparison-based sorting algorithms is defined: a sorting algorithm is a recursive datatype containing either a HOL function or a query of a comparison oracle with a continuation containing the remaining computation. This makes it possible to force the algorithm to use only comparisons and to track the number of comparisons made.
[Quick_Sort_Cost] title = The number of comparisons in QuickSort author = Manuel EberlWe give a formal proof of the well-known results about the number of comparisons performed by two variants of QuickSort: first, the expected number of comparisons of randomised QuickSort (i. e. QuickSort with random pivot choice) is 2 (n+1) Hn - 4 n, which is asymptotically equivalent to 2 n ln n; second, the number of comparisons performed by the classic non-randomised QuickSort has the same distribution in the average case as the randomised one.
[Random_BSTs] title = Expected Shape of Random Binary Search Trees author = Manuel EberlThis entry contains proofs for the textbook results about the distributions of the height and internal path length of random binary search trees (BSTs), i. e. BSTs that are formed by taking an empty BST and inserting elements from a fixed set in random order.
In particular, we prove a logarithmic upper bound on the expected height and the Θ(n log n) closed-form solution for the expected internal path length in terms of the harmonic numbers. We also show how the internal path length relates to the average-case cost of a lookup in a BST.
[Randomised_BSTs] title = Randomised Binary Search Trees author = Manuel EberlThis work is a formalisation of the Randomised Binary Search Trees introduced by Martínez and Roura, including definitions and correctness proofs.
Like randomised treaps, they are a probabilistic data structure that behaves exactly as if elements were inserted into a non-balancing BST in random order. However, unlike treaps, they only use discrete probability distributions, but their use of randomness is more complicated.
[E_Transcendental] title = The Transcendence of e author = Manuel EberlThis work contains a proof that Euler's number e is transcendental. The proof follows the standard approach of assuming that e is algebraic and then using a specific integer polynomial to derive two inconsistent bounds, leading to a contradiction.
This kind of approach can be found in many different sources; this formalisation mostly follows a PlanetMath article by Roger Lipsett.
[Pi_Transcendental] title = The Transcendence of π author = Manuel EberlThis entry shows the transcendence of π based on the classic proof using the fundamental theorem of symmetric polynomials first given by von Lindemann in 1882, but the formalisation mostly follows the version by Niven. The proof reuses much of the machinery developed in the AFP entry on the transcendence of e.
[Hermite_Lindemann] title = The Hermite–Lindemann–Weierstraß Transcendence Theorem author = Manuel EberlThis article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.
The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.
Like the previous formalisation in Coq by Bernard, I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.
This has a number of direct corollaries, e.g.:
This entry presents a framework for the modular verification of DFS-based algorithms, which is described in our [CPP-2015] paper. It provides a generic DFS algorithm framework, that can be parameterized with user-defined actions on certain events (e.g. discovery of new node). It comes with an extensible library of invariants, which can be used to derive invariants of a specific parameterization. Using refinement techniques, efficient implementations of the algorithms can easily be derived. Here, the framework comes with templates for a recursive and a tail-recursive implementation, and also with several templates for implementing the data structures required by the DFS algorithm. Finally, this entry contains a set of re-usable DFS-based algorithms, which illustrate the application of the framework.
[CPP-2015] Peter Lammich, René Neumann: A Framework for Verifying Depth-First Search Algorithms. CPP 2015: 137-146
[Flow_Networks] title = Flow Networks and the Min-Cut-Max-Flow Theorem author = Peter LammichThis article attempts to develop a usable framework for doing category theory in Isabelle/HOL. Our point of view, which to some extent differs from that of the previous AFP articles on the subject, is to try to explore how category theory can be done efficaciously within HOL, rather than trying to match exactly the way things are done using a traditional approach. To this end, we define the notion of category in an "object-free" style, in which a category is represented by a single partial composition operation on arrows. This way of defining categories provides some advantages in the context of HOL, including the ability to avoid the use of records and the possibility of defining functors and natural transformations simply as certain functions on arrows, rather than as composite objects. We define various constructions associated with the basic notions, including: dual category, product category, functor category, discrete category, free category, functor composition, and horizontal and vertical composite of natural transformations. A "set category" locale is defined that axiomatizes the notion "category of all sets at a type and all functions between them," and a fairly extensive set of properties of set categories is derived from the locale assumptions. The notion of a set category is used to prove the Yoneda Lemma in a general setting of a category equipped with a "hom embedding," which maps arrows of the category to the "universe" of the set category. We also give a treatment of adjunctions, defining adjunctions via left and right adjoint functors, natural bijections between hom-sets, and unit and counit natural transformations, and showing the equivalence of these definitions. We also develop the theory of limits, including representations of functors, diagrams and cones, and diagonal functors. We show that right adjoint functors preserve limits, and that limits can be constructed via products and equalizers. We characterize the conditions under which limits exist in a set category. We also examine the case of limits in a functor category, ultimately culminating in a proof that the Yoneda embedding preserves limits.
Revisions made subsequent to the first version of this article added material on equivalence of categories, cartesian categories, categories with pullbacks, categories with finite limits, and cartesian closed categories. A construction was given of the category of hereditarily finite sets and functions between them, and it was shown that this category is cartesian closed.
extra-history = Change history: [2018-05-29]: Revised axioms for the category locale. Introduced notation for composition and "in hom". (revision 8318366d4575)Building on the formalization of basic category theory set out in the author's previous AFP article, the present article formalizes some basic aspects of the theory of monoidal categories. Among the notions defined here are monoidal category, monoidal functor, and equivalence of monoidal categories. The main theorems formalized are MacLane's coherence theorem and the constructions of the free monoidal category and free strict monoidal category generated by a given category. The coherence theorem is proved syntactically, using a structurally recursive approach to reduction of terms that might have some novel aspects. We also give proofs of some results given by Etingof et al, which may prove useful in a formal setting. In particular, we show that the left and right unitors need not be taken as given data in the definition of monoidal category, nor does the definition of monoidal functor need to take as given a specific isomorphism expressing the preservation of the unit object. Our definitions of monoidal category and monoidal functor are stated so as to take advantage of the economy afforded by these facts.
Revisions made subsequent to the first version of this article added material on cartesian monoidal categories; showing that the underlying category of a cartesian monoidal category is a cartesian category, and that every cartesian category extends to a cartesian monoidal category.
extra-history = Change history: [2017-05-18]: Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter. (revision 015543cdd069)This entry provides three lemmas to count the number of multisets of a given size and finite carrier set. The first lemma provides a cardinality formula assuming that the multiset's elements are chosen from the given carrier set. The latter two lemmas provide formulas assuming that the multiset's elements also cover the given carrier set, i.e., each element of the carrier set occurs in the multiset at least once.
The proof of the first lemma uses the argument of the recurrence relation for counting multisets. The proof of the second lemma is straightforward, and the proof of the third lemma is easily obtained using the first cardinality lemma. A challenge for the formalization is the derivation of the required induction rule, which is a special combination of the induction rules for finite sets and natural numbers. The induction rule is derived by defining a suitable inductive predicate and transforming the predicate's induction rule.
[Posix-Lexing] title = POSIX Lexing with Derivatives of Regular Expressions author = Fahad AusafBrzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. 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. In this paper we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu’s algorithm always generates such a value (provided that the regular expression matches the string). This holds also when optimisations are included. Finally we show that (iii) our inductive definition of a POSIX value is equivalent to an alternative definition by Okui and Suzuki which identifies POSIX values as least elements according to an ordering of values.
[LocalLexing] title = Local Lexing author = Steven ObuaLiouville numbers are a class of transcendental numbers that can be approximated particularly well with rational numbers. Historically, they were the first numbers whose transcendence was proven.
In this entry, we define the concept of Liouville numbers as well as the standard construction to obtain Liouville numbers (including Liouville's constant) and we prove their most important properties: irrationality and transcendence.
The proof is very elementary and requires only standard arithmetic, the Mean Value Theorem for polynomials, and the boundedness of polynomials on compact intervals.
notify = manuel@pruvisto.org [Triangle] title = Basic Geometric Properties of Triangles author = Manuel EberlThis entry contains a definition of angles between vectors and between three points. Building on this, we prove basic geometric properties of triangles, such as the Isosceles Triangle Theorem, the Law of Sines and the Law of Cosines, that the sum of the angles of a triangle is π, and the congruence theorems for triangles.
The definitions and proofs were developed following those by John Harrison in HOL Light. However, due to Isabelle's type class system, all definitions and theorems in the Isabelle formalisation hold for all real inner product spaces.
notify = manuel@pruvisto.org [Prime_Harmonic_Series] title = The Divergence of the Prime Harmonic Series author = Manuel EberlIn this work, we prove the lower bound ln(H_n) - ln(5/3) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series ∑[p prime] · 1/p.
The proof relies on the unique squarefree decomposition of natural numbers. This is similar to Euler's original proof (which was highly informal and morally questionable). Its advantage over proofs by contradiction, like the famous one by Paul Erdős, is that it provides a relatively good lower bound for the partial sums.
notify = manuel@pruvisto.org [Descartes_Sign_Rule] title = Descartes' Rule of Signs author = Manuel EberlDescartes' Rule of Signs relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient sequence.
Our proof follows the simple inductive proof given by Rob Arthan, which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials.
notify = manuel@pruvisto.org [Euler_MacLaurin] title = The Euler–MacLaurin Formula author = Manuel EberlThe Euler-MacLaurin formula relates the value of a discrete sum to that of the corresponding integral in terms of the derivatives at the borders of the summation and a remainder term. Since the remainder term is often very small as the summation bounds grow, this can be used to compute asymptotic expansions for sums.
This entry contains a proof of this formula for functions from the reals to an arbitrary Banach space. Two variants of the formula are given: the standard textbook version and a variant outlined in Concrete Mathematics that is more useful for deriving asymptotic estimates.
As example applications, we use that formula to derive the full asymptotic expansion of the harmonic numbers and the sum of inverse squares.
[Card_Partitions] title = Cardinality of Set Partitions author = Lukas BulwahnThe classical definition of noninterference security for a deterministic state machine with outputs requires to consider the outputs produced by machine actions after any trace, i.e. any indefinitely long sequence of actions, of the machine. In order to render the verification of the security of such a machine more straightforward, there is a need of some sufficient condition for security such that just individual actions, rather than unbounded sequences of actions, have to be considered.
By extending previous results applying to transitive noninterference policies, Rushby has proven an unwinding theorem that provides a sufficient condition of this kind in the general case of a possibly intransitive policy. This condition has to be satisfied by a generic function mapping security domains into equivalence relations over machine states.
An analogous problem arises for CSP noninterference security, whose definition requires to consider any possible future, i.e. any indefinitely long sequence of subsequent events and any indefinitely large set of refused events associated to that sequence, for each process trace.
This paper provides a sufficient condition for CSP noninterference security, which indeed requires to just consider individual accepted and refused events and applies to the general case of a possibly intransitive policy. This condition follows Rushby's one for classical noninterference security, and has to be satisfied by a generic function mapping security domains into equivalence relations over process traces; hence its name, Generic Unwinding Theorem. Variants of this theorem applying to deterministic processes and trace set processes are also proven. Finally, the sufficient condition for security expressed by the theorem is shown not to be a necessary condition as well, viz. there exists a secure process such that no domain-relation map satisfying the condition exists.
notify = [Noninterference_Ipurge_Unwinding] title = The Ipurge Unwinding Theorem for CSP Noninterference Security author = Pasquale NoceThe definition of noninterference security for Communicating Sequential Processes requires to consider any possible future, i.e. any indefinitely long sequence of subsequent events and any indefinitely large set of refused events associated to that sequence, for each process trace. In order to render the verification of the security of a process more straightforward, there is a need of some sufficient condition for security such that just individual accepted and refused events, rather than unbounded sequences and sets of events, have to be considered.
Of course, if such a sufficient condition were necessary as well, it would be even more valuable, since it would permit to prove not only that a process is secure by verifying that the condition holds, but also that a process is not secure by verifying that the condition fails to hold.
This paper provides a necessary and sufficient condition for CSP noninterference security, which indeed requires to just consider individual accepted and refused events and applies to the general case of a possibly intransitive policy. This condition follows Rushby's output consistency for deterministic state machines with outputs, and has to be satisfied by a specific function mapping security domains into equivalence relations over process traces. The definition of this function makes use of an intransitive purge function following Rushby's one; hence the name given to the condition, Ipurge Unwinding Theorem.
Furthermore, in accordance with Hoare's formal definition of deterministic processes, it is shown that a process is deterministic just in case it is a trace set process, i.e. it may be identified by means of a trace set alone, matching the set of its traces, in place of a failures-divergences pair. Then, variants of the Ipurge Unwinding Theorem are proven for deterministic processes and trace set processes.
notify = [Relational_Method] title = The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols author = Pasquale NoceAmong the various mathematical tools introduced in his outstanding work on Communicating Sequential Processes, Hoare has defined "interleaves" as the predicate satisfied by any three lists such that the first list may be split into sublists alternately extracted from the other two ones, whatever is the criterion for extracting an item from either one list or the other in each step.
This paper enriches Hoare's definition by identifying such criterion with the truth value of a predicate taking as inputs the head and the tail of the first list. This enhanced "interleaves" predicate turns out to permit the proof of equalities between lists without the need of an induction. Some rules that allow to infer "interleaves" statements without induction, particularly applying to the addition or removal of a prefix to the input lists, are also proven. Finally, a stronger version of the predicate, named "Interleaves", is shown to fulfil further rules applying to the addition or removal of a suffix to the input lists.
notify = [Residuated_Lattices] title = Residuated Lattices author = Victor B. F. GomesWe use ConcurrentIMP to model Schism, a state-of-the-art real-time garbage collection scheme for weak memory, and show that it is safe on x86-TSO.
This development accompanies the PLDI 2015 paper of the same name.
notify = peteg42@gmail.com [List_Update] title = Analysis of List Update Algorithms author = Maximilian P.L. HaslbeckThese theories formalize the quantitative analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The material is based on the first two chapters of Online Computation and Competitive Analysis by Borodin and El-Yaniv.
For an informal description see the FSTTCS 2016 publication Verified Analysis of List Update Algorithms by Haslbeck and Nipkow.
notify = nipkow@in.tum.de [ConcurrentIMP] title = Concurrent IMP author = Peter GammieThe Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles.
This development mechanises an existing pen-and-paper proof of loop freedom of AODV. The protocol is modelled in the Algebra of Wireless Networks (AWN), which is the subject of an earlier paper and AFP mechanization. The proof relies on a novel compositional approach for lifting invariants to networks of nodes.
We exploit the mechanization to analyse several variants of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
notify = tim@tbrk.org [Show] title = Haskell's Show Class in Isabelle/HOL author = Christian SternagelIntransitive noninterference has been a widely studied topic in the last few decades. Several well-established methodologies apply interactive theorem proving to formulate a noninterference theorem over abstract academic models. In joint work with several industrial and academic partners throughout Europe, we are helping in the certification process of PikeOS, an industrial separation kernel developed at SYSGO. In this process, established theories could not be applied. We present a new generic model of separation kernels and a new theory of intransitive noninterference. The model is rich in detail, making it suitable for formal verification of realistic and industrial systems such as PikeOS. Using a refinement-based theorem proving approach, we ensure that proofs remain manageable.
This document corresponds to the deliverable D31.1 of the EURO-MILS Project http://www.euromils.eu.
notify = [pGCL] title = pGCL for Isabelle author = David CockpGCL is both a programming language and a specification language that incorporates both probabilistic and nondeterministic choice, in a unified manner. Program verification is by refinement or annotation (or both), using either Hoare triples, or weakest-precondition entailment, in the style of GCL.
This package provides both a shallow embedding of the language primitives, and an annotation and refinement framework. The generated document includes a brief tutorial.
notify = [Noninterference_CSP] title = Noninterference Security in Communicating Sequential Processes author = Pasquale NoceAn extension of classical noninterference security for deterministic state machines, as introduced by Goguen and Meseguer and elegantly formalized by Rushby, to nondeterministic systems should satisfy two fundamental requirements: it should be based on a mathematically precise theory of nondeterminism, and should be equivalent to (or at least not weaker than) the classical notion in the degenerate deterministic case.
This paper proposes a definition of noninterference security applying to Hoare's Communicating Sequential Processes (CSP) in the general case of a possibly intransitive noninterference policy, and proves the equivalence of this security property to classical noninterference security for processes representing deterministic state machines.
Furthermore, McCullough's generalized noninterference security is shown to be weaker than both the proposed notion of CSP noninterference security for a generic process, and classical noninterference security for processes representing deterministic state machines. This renders CSP noninterference security preferable as an extension of classical noninterference security to nondeterministic systems.
notify = pasquale.noce.lavoro@gmail.com [Floyd_Warshall] title = The Floyd-Warshall Algorithm for Shortest Paths author = Simon WimmerAWN is a process algebra developed for modelling and analysing protocols for Mobile Ad hoc Networks (MANETs) and Wireless Mesh Networks (WMNs). AWN models comprise five distinct layers: sequential processes, local parallel compositions, nodes, partial networks, and complete networks.
This development mechanises the original operational semantics of AWN and introduces a variant 'open' operational semantics that enables the compositional statement and proof of invariants across distinct network nodes. It supports labels (for weakening invariants) and (abstract) data state manipulations. A framework for compositional invariant proofs is developed, including a tactic (inv_cterms) for inductive invariant proofs of sequential processes, lifting rules for the open versions of the higher layers, and a rule for transferring lifted properties back to the standard semantics. A notion of 'control terms' reduces proof obligations to the subset of subterms that act directly (in contrast to operators for combining terms and joining processes).
notify = tim@tbrk.org [Selection_Heap_Sort] title = Verification of Selection and Heap Sort Using Locales author = Danijela Petrovic
Our results have been used to certify termination proofs which involve
polynomial interpretations over the reals.
extra-history =
Change history:
[2014-07-11]: Moved NthRoot_Impl to Sqrt-Babylonian.
notify = rene.thiemann@uibk.ac.at
[ShortestPath]
title = An Axiomatic Characterization of the Single-Source Shortest Path Problem
author = Christine Rizkallah
We use syntax and the denotational semantics from the entry
"Launchbury", where we formalized Launchbury's natural semantics for
lazy evaluation.
The functional correctness of Call Arity is proved with regard to that
denotational semantics. The operational properties are shown with
regard to a small-step semantics akin to Sestoft's mark 1 machine,
which we prove to be equivalent to Launchbury's semantics.
We use Christian Urban's Nominal2 package to define our terms and make
use of Brian Huffman's HOLCF package for the domain-theoretical
aspects of the development.
extra-history =
Change history:
[2015-03-16]: This entry now builds on top of the Launchbury entry,
and the equivalency proof of the natural and the small-step semantics
was added.
notify =
[CCS]
title = CCS in nominal logic
author = Jesper Bengtson
This entry is described in detail in Bengtson's thesis.
notify =
[Pi_Calculus]
title = The pi-calculus in nominal logic
author = Jesper Bengtson
A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.
This entry is described in detail in Bengtson's thesis.
notify =
[Psi_Calculi]
title = Psi-calculi in Isabelle
author = Jesper Bengtson
We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.
The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. This includes treating all binding sequences as atomic elements, and creating custom induction and inversion rules that to remove the bulk of manual alpha-conversions.
This entry is described in detail in Bengtson's thesis.
notify =
[Encodability_Process_Calculi]
title = Analysing and Comparing Encodability Criteria for Process Calculi
author = Kirstin Peters
The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.
extra-history =
Change history:
[2014-06-05]: More polishing, shorter proofs, added Circus syntax, added Makarius Wenzel as contributor.
notify =
[Dijkstra_Shortest_Path]
title = Dijkstra's Shortest Path Algorithm
author = Benedikt Nordhoff
The framework provides tools to automatize canonical tasks, such as
verification condition generation, finding appropriate data refinement relations,
and refine an executable program to a form that is accepted by the
Isabelle/HOL code generator.
This submission comes with a collection of examples and a user-guide,
illustrating the usage of the framework.
extra-history =
Change history:
[2012-04-23] Introduced ordered FOREACH loops
This AFP-entry provides the basic tool, which is then used by the
Refinement and Collection Framework to provide automatic data refinement for
the nondeterminism monad and various collection datastructures.
notify = lammich@in.tum.de
[EdmondsKarp_Maxflow]
title = Formalizing the Edmonds-Karp Algorithm
author = Peter Lammich
An earlier version of this work was the subject of the author's
MSc thesis,
which contains natural-language explanations of some of the
more interesting proofs.
notify = tjm1983@gmail.com
[IsaGeoCoq]
title = Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid
author = Roland Coghetto The GeoCoq library contains a formalization
of geometry using the Coq proof assistant. It contains both proofs
about the foundations of geometry and high-level proofs in the same
style as in high school. We port a part of the GeoCoq
2.4.0 library to Isabelle/HOL: more precisely,
the files Chap02.v to Chap13_3.v, suma.v as well as the associated
definitions and some useful files for the demonstration of certain
parallel postulates. The synthetic approach of the demonstrations is directly
inspired by those contained in GeoCoq. The names of the lemmas and
theorems used are kept as far as possible as well as the definitions.
It should be noted that T.J.M. Makarios has done
some proofs in Tarski's Geometry. It uses a definition that does not quite
coincide with the definition used in Geocoq and here.
Furthermore, corresponding definitions in the Poincaré Disc Model
development are not identical to those defined in GeoCoq.
In the last part, it is
formalized that, in the neutral/absolute space, the axiom of the
parallels of Tarski's system implies the Playfair axiom, the 5th
postulate of Euclid and Euclid's original parallel postulate. These
proofs, which are not constructive, are directly inspired by Pierre
Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.
extra-history =
Change history:
[2011-08-26]: Christian Urban added a theory about derivatives and partial derivatives of regular expressions
Decision procedures for regular expression equivalence have been formalized
before, usually based on Brzozowski derivatives. Yet, for a straightforward
embedding of MSO formulas into regular expressions an extension of regular
expressions with a projection operation is required. We prove total
correctness and completeness of an equivalence checker for regular
expressions extended in that way. We also define a language-preserving
translation of formulas into regular expressions with respect to two
different semantics of MSO.
The formalization is described in this ICFP 2013 functional pearl.
notify = traytel@in.tum.de, nipkow@in.tum.de
[Formula_Derivatives]
title = Derivatives of Logical Formulas
author = Dmitriy Traytel
The WS1S instance is described in the draft paper A
Coalgebraic Decision Procedure for WS1S by the author.
notify = traytel@in.tum.de
[Myhill-Nerode]
title = The Myhill-Nerode Theorem Based on Regular Expressions
author = Chunhan Wu <>, Xingyuan Zhang <>, Christian Urban Two omega-sequences are stuttering equivalent if they differ only by finite repetitions of elements. Stuttering equivalence is a fundamental concept in the theory of concurrent and distributed systems. Notably, Lamport argues that refinement notions for such systems should be insensitive to finite stuttering. Peled and Wilke showed that all PLTL (propositional linear-time temporal logic) properties that are insensitive to stuttering equivalence can be expressed without the next-time operator. Stuttering equivalence is also important for certain verification techniques such as partial-order reduction for model checking. We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of stuttering sampling functions that may skip blocks of identical sequence elements. We also encode PLTL and prove the theorem due to Peled and Wilke. We define formal languages as a codataype of infinite trees
branching over the alphabet. Each node in such a tree indicates whether the
path to this node constitutes a word inside or outside of the language. This
codatatype is isormorphic to the set of lists representation of languages,
but caters for definitions by corecursion and proofs by coinduction. Regular operations on languages are then defined by primitive corecursion.
A difficulty arises here, since the standard definitions of concatenation and
iteration from the coalgebraic literature are not primitively
corecursive-they require guardedness up-to union/concatenation.
Without support for up-to corecursion, these operation must be defined as a
composition of primitive ones (and proved being equal to the standard
definitions). As an exercise in coinduction we also prove the axioms of
Kleene algebra for the defined regular operations. Furthermore, a language for context-free grammars given by productions in
Greibach normal form and an initial nonterminal is constructed by primitive
corecursion, yielding an executable decision procedure for the word problem
without further ado.
The UpDown scheme allows us to compute the stiffness matrix on such a sparse
grid. The stiffness matrix represents the influence of each representation
function on the L^2 scalar product. For a detailed description see
Dirk Pflüger's PhD thesis. This formalization was developed as an
interdisciplinary project (IDP) at the Technische Universität München.
notify = hoelzl@in.tum.de
[GraphMarkingIBP]
title = Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
author = Viorel Preoteasa
We provide a generic work-list algorithm to compute the
(reflexive-)transitive closure of relations where only successors of newly
detected states are generated.
In contrast to our previous work, the relations do not have to be finite,
but each element must only have finitely many (indirect) successors.
Moreover, a subsumption relation can be used instead of pure equality.
An executable variant of the algorithm is available where the generic operations
are instantiated with list operations.
This formalization was performed as part of the IsaFoR/CeTA project,
and it has been used to certify size-change
termination proofs where large transitive closures have to be computed.
Indeed, there have been numerous misunderstandings on what exactly a given
algorithm is supposed to realize in what kinds of environments. Moreover, the
abundance of subtly different computational models complicates comparisons
between different algorithms. Charron-Bost and Schiper introduced the Heard-Of
model for representing algorithms and failure assumptions in a uniform
framework, simplifying comparisons between algorithms.
In this contribution, we represent the Heard-Of model in Isabelle/HOL. We define
two semantics of runs of algorithms with different unit of atomicity and relate
these through a reduction theorem that allows us to verify algorithms in the
coarse-grained semantics (where proofs are easier) and infer their correctness
for the fine-grained one (which corresponds to actual executions). We
instantiate the framework by verifying six Consensus algorithms that differ in
the underlying algorithmic mechanisms and the kinds of faults they tolerate.
notify = Stephan.Merz@loria.fr
[Consensus_Refined]
title = Consensus Refined
date = 2015-03-18
author = Ognjen Maric <>, Christoph Sprenger
A preliminary version of this work (without pairing heaps) is described
in a paper
published in the proceedings of the conference on Interactive
Theorem Proving ITP 2015. An extended version of this publication
is available here.
extra-history =
Change history:
[2015-03-17]: Added pairing heaps by Hauke Brinkop.
A full description is found in a
companion paper.
notify = nipkow@in.tum.de
[AVL-Trees]
title = AVL Trees
author = Tobias Nipkow
The amortized complexity of splay trees and heaps is analyzed in the AFP entry
Amortized Complexity.
extra-history =
Change history:
[2016-07-12]: Moved splay heaps here from Amortized_Complexity
[Root_Balanced_Tree]
title = Root-Balanced Tree
author = Tobias Nipkow
Andersson introduced general balanced trees,
search trees based on the design principle of partial rebuilding:
perform update operations naively until the tree becomes too
unbalanced, at which point a whole subtree is rebalanced. This article
defines and analyzes a functional version of general balanced trees,
which we call root-balanced trees. Using a lightweight model
of execution time, amortized logarithmic complexity is verified in
the theorem prover Isabelle.
This is the Isabelle formalization of the material decribed in the APLAS 2017 article
Verified Root-Balanced Trees
by the same author, which also presents experimental results that show
competitiveness of root-balanced with AVL and red-black trees.
The amortized complexity of skew heaps is analyzed in the AFP entry
Amortized Complexity.
notify = nipkow@in.tum.de
[Pairing_Heap]
title = Pairing Heap
author = Hauke Brinkop
The amortized complexity of pairing heaps is analyzed in the AFP article
Amortized Complexity.
extra-0 = Origin: This library was extracted from Amortized Complexity and extended.
notify = nipkow@in.tum.de
[Priority_Queue_Braun]
title = Priority Queues Based on Braun Trees
author = Tobias Nipkow
To support arbitrary nesting of sets, we define a linear order on sets based on a linear order of the elements and provide efficient implementations.
It even allows to compare complements with non-complements.
extra-history =
Change history:
[2013-07-11]: add pretty printing for sets (revision 7f3f52c5f5fa)
We further implemented such automatic methods to derive (linear) orders or hash-functions which are
required in the Isabelle Collection Framework. Moreover, for the tactic of Huffman and Krauss to show that a
datatype is countable, we implemented a wrapper so that this tactic becomes accessible in our framework.
Our formalization was performed as part of the IsaFoR/CeTA project.
With our new tactic we could completely remove
tedious proofs for linear orders of two datatypes.
This development is aimed at datatypes generated by the "old_datatype"
command.
notify = rene.thiemann@uibk.ac.at
[Deriving]
title = Deriving class instances for datatypes
author = Christian Sternagel We provide a framework for registering automatic methods
to derive class instances of datatypes,
as it is possible using Haskell's ``deriving Ord, Show, ...'' feature. We further implemented such automatic methods to derive comparators, linear orders, parametrizable equality functions,
and hash-functions which are required in the
Isabelle Collection Framework and the Container Framework.
Moreover, for the tactic of Blanchette to show that a datatype is countable, we implemented a
wrapper so that this tactic becomes accessible in our framework. All of the generators are based on
the infrastructure that is provided by the BNF-based datatype package. Our formalization was performed as part of the IsaFoR/CeTA project.
With our new tactics we could remove
several tedious proofs for (conditional) linear orders, and conditional equality operators
within IsaFoR and the Container Framework.
In principle, such a definition is also directly possible using the
lift_definition command. However, then this definition will not be
suitable for code-generation. To this end, we automated a more complex
construction of Joachim Breitner which is amenable for code-generation, and
where the test check ys will only be performed once. In the
automation, one auxiliary type is created, and Isabelle's lifting- and
transfer-package is invoked several times.
notify = rene.thiemann@uibk.ac.at
[Coinductive]
title = Coinductive
topic = Computer science/Functional programming
author = Andreas Lochbihler
Based on the hierarchy of type classes in Haskell, we define classes
for functors, monads, monad-plus, etc. Each one includes all the
standard laws as axioms. We also provide a new user command,
tycondef, for defining new type constructors in HOLCF. Using tycondef,
we instantiate the type class hierarchy with various monads and monad
transformers.
notify = huffman@in.tum.de
[CoreC++]
title = CoreC++
author = Daniel Wasserrab
Consequently the package is geared towards
parsing, printing and code-generation to the Isabelle API.
It is at the moment not sufficiently rich for doing meta theory on
Isabelle itself. Extensions in this direction are possible though.
Moreover, the chosen fragment is fairly rudimentary. However it should be
easily adapted to one's needs if a package is written on top of it.
The supported API contains types, terms, transformation of
global context like definitions and data-type declarations as well
as infrastructure for Isar-setups.
This theory is drawn from the
Featherweight OCL
project where
it is used to construct a package for object-oriented data-type theories
generated from UML class diagrams. The Featherweight OCL, for example, allows for
both the direct execution of compiled tactic code by the Isabelle API
as well as the generation of ".thy"-files for debugging purposes.
Gained experience from this project shows that the compiled code is sufficiently
efficient for practical purposes while being based on a formal model
on which properties of the package can be proven such as termination of certain
transformations, correctness, etc.
notify = tuong@users.gforge.inria.fr, wolff@lri.fr
[Clean]
title = Clean - An Abstract Imperative Programming Language and its Theory
author = Frédéric Tuong The ex directory contains example instantiations that include structures such as a heap or virtual memory. The abstract separation algebra is based upon "Abstract Separation Logic" by Calcagno et al. These theories are also the basis of the ITP 2012 rough diamond "Mechanised Separation Algebra" by the authors. The aim of this work is to support and significantly reduce the effort for future separation logic developments in Isabelle/HOL by factoring out the part of separation logic that can be treated abstractly once and for all. This includes developing typical default rule sets for reasoning as well as automated tactic support for separation logic.
notify = kleing@cse.unsw.edu.au, rafal.kolanski@nicta.com.au
[Separation_Logic_Imperative_HOL]
title = A Separation Logic Framework for Imperative HOL
author = Peter Lammich
An article
about these proofs is published in the proceedings
of the conference Certified Programs and Proofs 2012.
notify = hoelzl@in.tum.de
[SIFUM_Type_Systems]
title = A Formalization of Assumptions and Guarantees for Compositional Noninterference
author = Sylvia Grewe
[2012-06] New features:
REC_rule_arb and RECT_rule_arb allow for generalizing over variables.
prepare_code_thms - command extracts code equations for recursion combinators.
[2012-07] New example: Nested DFS for emptiness check of Buchi-automata with witness.
New feature:
fo_rule method to apply resolution using first-order matching. Useful for arg_conf, fun_cong.
[2012-08] Adaptation to ICF v2.
[2012-10-05] Adaptations to include support for Automatic Refinement Framework.
[2013-09] This entry now depends on Automatic Refinement
[2014-06] New feature: vc_solve method to solve verification conditions.
Maintenace changes: VCG-rules for nfoldli, improved setup for FOREACH-loops.
[2014-07] Now defining recursion via flat domain. Dropped many single-valued prerequisites.
Changed notion of data refinement. In single-valued case, this matches the old notion.
In non-single valued case, the new notion allows for more convenient rules.
In particular, the new definitions allow for projecting away ghost variables as a refinement step.
[2014-11] New features: le-or-fail relation (leof), modular reasoning about loop invariants.
notify = lammich@in.tum.de
[Refine_Imperative_HOL]
title = The Imperative Refinement Framework
author = Peter Lammich
[2012-05-10]: Tobias Nipkow added extended regular expressions
[2012-05-10]: Tobias Nipkow added equivalence checking with partial derivatives
notify = nipkow@in.tum.de, krauss@in.tum.de, christian.urban@kcl.ac.uk
[Regex_Equivalence]
title = Unified Decision Procedures for Regular Expression Equivalence
author = Tobias Nipkow
[2018-09-17]:
Added theory Efficient_Mergesort that works exclusively with the mutual
induction schemas generated by the function package.
[2018-09-19]:
Added theory Mergesort_Complexity that proves an upper bound on the number of
comparisons that are required by mergesort.
[2018-09-19]:
Theory Efficient_Mergesort replaces theory Efficient_Sort but keeping the old
name Efficient_Sort.
[2020-11-20]:
Additional theory Natural_Mergesort that developes an efficient mergesort
algorithm without key-functions for educational purposes.
notify = c.sternagel@gmail.com
[SATSolverVerification]
title = Formal Verification of Modern SAT Solvers
author = Filip Marić
Within the SAT solver correctness proofs, a large number of lemmas about propositional logic and CNF formulae are proved. This theory is self-contained and could be used for further exploring of properties of CNF based SAT algorithms.
notify =
[Transitive-Closure]
title = Executable Transitive Closures of Finite Relations
topic = Computer science/Algorithms/Graph
date = 2011-03-14
author = Christian Sternagel
[2016-07-12]: Moved splay heaps from here to Splay_Tree
[2016-07-14]: Moved pairing heaps from here to the new Pairing_Heap
notify = nipkow@in.tum.de
[Dynamic_Tables]
title = Parameterized Dynamic Tables
author = Tobias Nipkow
[2010-11-04]:
new conversion function from FinFun to list of elements in the domain
(revision 0c167102e6ed)
[2012-03-07]:
replace sets as FinFuns by predicates as FinFuns because the set type constructor has been reintroduced
(revision b7aa87989f3a)
notify = nipkow@in.tum.de
[Collections]
title = Collections Framework
author = Peter Lammich
[2010-12-01]: New Interfaces: Priority Queues, Annotated Lists. Implemented by finger trees, (skew) binomial queues.
[2011-10-10]: SetSpec: Added operations: sng, isSng, bexists, size_abort, diff, filter, iterate_rule_insertP
MapSpec: Added operations: sng, isSng, iterate_rule_insertP, bexists, size, size_abort, restrict,
map_image_filter, map_value_image_filter
Some maintenance changes
[2012-04-25]: New iterator foundation by Tuerk. Various maintenance changes.
[2012-08]: Collections V2. New features: Polymorphic iterators. Generic algorithm instantiation where required. Naming scheme changed from xx_opname to xx.opname.
A compatibility file CollectionsV1 tries to simplify porting of existing theories, by providing old naming scheme and the old monomorphic iterator locales.
[2013-09]: Added Generic Collection Framework based on Autoref. The GenCF provides: Arbitrary nesting, full integration with Autoref.
[2014-06]: Maintenace changes to GenCF: Optimized inj_image on list_set. op_set_cart (Cartesian product). big-Union operation. atLeastLessThan - operation ({a..<b})
notify = lammich@in.tum.de
[Containers]
title = Light-weight Containers
author = Andreas Lochbihler
[2013-09-20]:
provide generators for canonical type class instantiations
(revision 159f4401f4a8 by René Thiemann)
[2014-07-08]: add support for going from partial functions to mappings (revision 7a6fc957e8ed)
[2018-03-05]: add two application examples: depth-first search and 2SAT (revision e5e1a1da2411)
notify = mail@andreas-lochbihler.de
[FileRefinement]
title = File Refinement
author = Karen Zee
The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
extra-history =
Change history:
[2010-06-10]:
coinductive lists: setup for quotient package
(revision 015574f3bf3c)
[2010-06-28]:
new codatatype terminated lazy lists
(revision e12de475c558)
[2010-08-04]:
terminated lazy lists: setup for quotient package;
more lemmas
(revision 6ead626f1d01)
[2010-08-17]:
Koenig's lemma as an example application for coinductive lists
(revision f81ce373fa96)
[2011-02-01]:
lazy implementation of coinductive (terminated) lists for the code generator
(revision 6034973dce83)
[2011-07-20]:
new codatatype resumption
(revision 811364c776c7)
[2012-06-27]:
new codatatype stream with operations (with contributions by Peter Gammie)
(revision dd789a56473c)
[2013-03-13]:
construct codatatypes with the BNF package and adjust the definitions and proofs,
setup for lifting and transfer packages
(revision f593eda5b2c0)
[2013-09-20]:
stream theory uses type and operations from HOL/BNF/Examples/Stream
(revision 692809b2b262)
[2014-04-03]:
ccpo structure on codatatypes used to define ldrop, ldropWhile, lfilter, lconcat as least fixpoint;
ccpo topology on coinductive lists contributed by Johannes Hölzl;
added examples
(revision 23cd8156bd42)
notify = mail@andreas-lochbihler.de
[Stream-Fusion]
title = Stream Fusion
author = Brian Huffman
These theories contain a formalization of much of the Stream Fusion library in HOLCF. Lazy list and stream types are defined, along with coercions between the two types, as well as an equivalence relation for streams that generate the same list. List and stream versions of map, filter, foldr, enumFromTo, append, zipWith, and concatMap are defined, and the stream versions are shown to respect stream equivalence.
notify = brianh@cs.pdx.edu
[Tycon]
title = Type Constructor Classes and Monad Transformers
author = Brian Huffman
[2009-04-27]:
added verified compiler from source code to bytecode;
encapsulate native methods in separate semantics
(revision e4f26541e58a)
[2009-11-30]:
extended compiler correctness proof to infinite and deadlocking computations
(revision e50282397435)
[2010-06-08]:
added thread interruption;
new abstract memory model with sequential consistency as implementation
(revision 0cb9e8dbd78d)
[2010-06-28]:
new thread interruption model
(revision c0440d0a1177)
[2010-10-15]:
preliminary version of the Java memory model for source code
(revision 02fee0ef3ca2)
[2010-12-16]:
improved version of the Java memory model, also for bytecode
executable scheduler for source code semantics
(revision 1f41c1842f5a)
[2011-02-02]:
simplified code generator setup
new random scheduler
(revision 3059dafd013f)
[2011-07-21]:
new interruption model,
generalized JMM proof of DRF guarantee,
allow class Object to declare methods and fields,
simplified subtyping relation,
corrected division and modulo implementation
(revision 46e4181ed142)
[2012-02-16]:
added example programs
(revision bf0b06c8913d)
[2012-11-21]:
type safety proof for the Java memory model,
allow spurious wake-ups
(revision 76063d860ae0)
[2013-05-16]:
support for non-deterministic memory allocators
(revision cc3344a49ced)
[2017-10-20]:
add an atomic compare-and-swap operation for volatile fields
(revision a6189b1d6b30)
notify = mail@andreas-lochbihler.de
[Locally-Nameless-Sigma]
title = Locally Nameless Sigma Calculus
author = Ludovic Henrio
As we target Imperative HOL, our programs can be translated to
efficiently executable code in various target languages, including
ML, OCaml, Haskell, and Scala.
notify = lammich@in.tum.de
[Inductive_Confidentiality]
title = Inductive Study of Confidentiality
author = Giampaolo Bella