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 x^{2} = 1 + D y^{2}, 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 (x_{0}, y_{0}) 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 = (x_{0} + y_{0} √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.
[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 2^{n} 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 log_{2} (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) H_{n} - 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 AusafLiouville 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 = eberlm@in.tum.de [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 = eberlm@in.tum.de [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 = eberlm@in.tum.de [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 = eberlm@in.tum.de [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
[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
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.
[General-Triangle] title = The General Triangle Is Unique author = Joachim Breitner 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
[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
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.
extra-history = Change history: [2013-01-31]: Added encoding of PLTL and proved Peled and Wilke's theorem. Adjusted abstract accordingly. notify = Stephan.Merz@loria.fr [Coinductive_Languages] title = A Codatatype of Formal Languages author = Dmitriy TraytelWe 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.
notify = traytel@in.tum.de [Tree-Automata] title = Tree Automata author = Peter Lammich
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
[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ć
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.
notify = rene.thiemann@uibk.ac.at [MuchAdoAboutTwo] title = Much Ado About Two author = Sascha BöhmeIndeed, 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.
[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
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.
[Skew_Heap] title = Skew Heap author = Tobias Nipkow
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
[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
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)
[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
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.
notify = rene.thiemann@uibk.ac.at [List-Index] title = List Index date = 2010-02-20 author = Tobias Nipkow
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
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
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
[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
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
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
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
The paper "Assumptions and Guarantees for Compositional
Noninterference" by Mantel et. al. presents one solution for this problem:
an approach for compositionally reasoning about non-interference in
concurrent programs via rely-guarantee-style reasoning. We present an
Isabelle/HOL formalization of the concepts and proofs of this approach.
notify =
[Dependent_SIFUM_Type_Systems]
title = A Dependent Security Type System for Concurrent Imperative Programs
author = Toby Murray
We present an Isabelle/HOL formalization of strong security for arbitrary security lattices (Sabelfeld and Sands use a two-element security lattice in the original publication). The formalization includes compositionality proofs for strong security and a soundness proof for a security type system that checks strong security for programs in a simple while language with dynamic thread creation.
Our formalization of the security type system is abstract in the
language for expressions and in the semantic side conditions for
expressions. It can easily be instantiated with different syntactic
approximations for these side conditions. The soundness proof of
such an instantiation boils down to showing that these syntactic
approximations imply the semantic side conditions.
notify =
[WHATandWHERE_Security]
title = A Formalization of Declassification with WHAT-and-WHERE-Security
author = Sylvia Grewe
We present an Isabelle/HOL formalization of such a security property for controlled declassification, namely WHAT&WHERE-security from "Scheduler-Independent Declassification" by Lux, Mantel, and Perner. The formalization includes compositionality proofs for and a soundness proof for a security type system that checks for programs in a simple while language with dynamic thread creation.
Our formalization of the security type system is abstract in the language for expressions and in the semantic side conditions for expressions. It can easily be instantiated with different syntactic approximations for these side conditions. The soundness proof of such an instantiation boils down to showing that these syntactic approximations imply the semantic side conditions.
This Isabelle/HOL formalization uses theories from the entry
Strong Security.
notify =
[VolpanoSmith]
title = A Correctness Proof for the Volpano/Smith Security Typing System
author = Gregor Snelting
We start with formalising dioids, which are additively idempotent semirings, and expand them by axiomatisations of the Kleene star for finite iteration and an omega operation for infinite iteration. We show that powersets over a given monoid, (regular) languages, sets of paths in a graph, sets of computation traces, binary relations and formal power series form Kleene algebras, and consider further models based on lattices, max-plus semirings and min-plus semirings. We also demonstrate that dioids are closed under the formation of matrices (proofs for Kleene algebras remain to be completed).
On the one hand we have aimed at a reference formalisation of variants
of Kleene algebras that covers a wide range of variants and the core
theorems in a structured and modular way and provides readable proofs
at text book level. On the other hand, we intend to use this algebraic
hierarchy and its models as a generic algebraic middle-layer from which
programming applications can quickly be explored, implemented and verified.
notify = g.struth@sheffield.ac.uk, tjark.weber@it.uu.se
[KAT_and_DRA]
title = Kleene Algebra with Tests and Demonic Refinement Algebras
author = Alasdair Armstrong <>, Victor B. F. Gomes
The present proof development represents an update of the formalisation underlying our paper [CSF 2007] and is intended to resolve any ambiguities that may be present in the paper.
notify = lennart.beringer@ifi.lmu.de
[TLA]
title = A Definitional Encoding of TLA* in Isabelle/HOL
author = Gudmund Grov
In this contribution, we show how correctness proofs for intra- and interprocedural slicing can be used to prove that slicing is able to guarantee information flow noninterference. Moreover, we also illustrate how to lift the control flow graphs of the respective frameworks such that they fulfil the additional assumptions needed in the noninterference proofs. A detailed description of the intraprocedural proof and its interplay with the slicing framework can be found in the PLAS'09 paper by Wasserrab et al.
This entry contains the part for intra-procedural slicing. See entry InformationFlowSlicing_Inter for the inter-procedural part.
extra-history = Change history: [2016-06-10]: The original entry InformationFlowSlicing contained both the inter- and intra-procedural case was split into two for easier maintenance. notify = [InformationFlowSlicing_Inter] title = Inter-Procedural Information Flow Noninterference via Slicing author = Daniel WasserrabIn this contribution, we show how correctness proofs for intra- and interprocedural slicing can be used to prove that slicing is able to guarantee information flow noninterference. Moreover, we also illustrate how to lift the control flow graphs of the respective frameworks such that they fulfil the additional assumptions needed in the noninterference proofs. A detailed description of the intraprocedural proof and its interplay with the slicing framework can be found in the PLAS'09 paper by Wasserrab et al.
This entry contains the part for inter-procedural slicing. See entry InformationFlowSlicing for the intra-procedural part.
extra-history = Change history: [2016-06-10]: The original entry InformationFlowSlicing contained both the inter- and intra-procedural case was split into two for easier maintenance. notify = [ComponentDependencies] title = Formalisation and Analysis of Component Dependencies author = Maria SpichkovaEssentially, the encodings proceed as follows: a many-sorted problem is decorated with (as few as possible) tags or guards that make the problem monotonic; then sorts can be soundly erased.
The development employs a formalization of many-sorted first-order logic
in clausal form (clauses, structures and the basic properties
of the satisfaction relation), which could be of interest as the starting
point for other formalizations of first-order logic metatheory.
notify = uuomul@yahoo.com
[Lambda_Free_RPOs]
title = Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
author = Jasmin Christian Blanchette
[2013-10-16]: Generalized delta-orders from rationals to Archimedean fields.
notify = christian.sternagel@uibk.ac.at, rene.thiemann@uibk.ac.at
[First_Order_Terms]
title = First-Order Terms
author = Christian Sternagel
[2017-09-20]: linear approximations for all symbols from the floatarith data
type
notify = immler@in.tum.de
[Laplace_Transform]
title = Laplace Transform
author = Fabian Immler
Session Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.
Not in the generated document are the following sessions:
This formalization also contains an abstract representation as coefficient functions with finite
support and a type of power-products. If this type is ordered by a linear (term) ordering, various
additional notions, such as leading power-product, leading coefficient etc., are introduced as
well. Furthermore, a lot of generic properties of, and functions on, multivariate polynomials are
formalized, including the substitution and evaluation homomorphisms, embeddings of polynomial rings
into larger rings (i.e. with one additional indeterminate), homogenization and dehomogenization of
polynomials, and the canonical isomorphism between R[X,Y] and R[X][Y].
extra-history =
Change history:
[2010-09-17]: Moved theories on arbitrary (ordered) semirings to Abstract Rewriting.
[2016-10-28]: Added abstract representation of polynomials and authors Maletzky/Immler.
[2018-01-23]: Added authors Haftmann, Lochbihler after incorporating
their formalization of multivariate polynomials based on Polynomial mappings.
Moved material from Bentkamp's entry "Deep Learning".
[2019-04-18]: Added material about polynomials whose power-products are represented themselves
by polynomial mappings.
notify = rene.thiemann@uibk.ac.at, christian.sternagel@uibk.ac.at, alexander.maletzky@risc.jku.at, immler@in.tum.de
[Sqrt_Babylonian]
title = Computing N-th Roots using the Babylonian Method
author = René Thiemann
As application of these models we formalize probabilistic model
checking of pCTL formulas, analysis of IPv4 address allocation in
ZeroConf and an analysis of the anonymity of the Crowds protocol.
See here for the corresponding paper.
notify = hoelzl@in.tum.de
[Probabilistic_System_Zoo]
title = A Zoo of Probabilistic Systems
author = Johannes Hölzl
This work is described in detail in the ITP 2015 publication by the authors.
notify = traytel@in.tum.de
[Density_Compiler]
title = A Verified Compiler for Probability Density Functions
author = Manuel Eberl
An article with the same title and authors is published in the proceedings
of ESOP 2015.
A detailed presentation of this work can be found in the first author's
master's thesis.
notify = hoelzl@in.tum.de
[CAVA_Automata]
title = The CAVA Automata Library
author = Peter Lammich
The CAVA Automata Library provides a hierarchy of graph and automata classes, together with some standard algorithms. Its object oriented design allows for sharing of algorithms, theorems, and implementations between its classes, and also simplifies extensions of the library. Moreover, it is integrated into the Automatic Refinement Framework, supporting automatic refinement of the abstract automata types to efficient data structures.
Note that the CAVA Automata Library is work in progress. Currently, it is very specifically tailored towards the requirements of the CAVA model checker. Nevertheless, the formalization techniques presented here allow an extension of the library to a wider scope. Moreover, they are not limited to graph libraries, but apply to class hierarchies in general.
The CAVA Automata Library is described in the paper: Peter Lammich, The
CAVA Automata Library, Isabelle Workshop 2014.
notify = lammich@in.tum.de
[LTL]
title = Linear Temporal Logic
author = Salomon Sickert
notify = sickert@in.tum.de
[LTL_to_GBA]
title = Converting Linear-Time Temporal Logic to Generalized Büchi Automata
author = Alexander Schimpf
We use the Isabelle Refinement and Collection framework, as well as the
Autoref tool, to obtain a refined version of our algorithm, from which
efficiently executable code can be extracted.
notify = lammich@in.tum.de
[Gabow_SCC]
title = Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
author = Peter Lammich
An early version of this model checker is described in the CAV 2013 paper with the same title. notify = lammich@in.tum.de [Fermat3_4] title = Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples author = Roelof Oosterhuis <> date = 2007-08-12 topic = Mathematics/Number theory abstract = This document presents the mechanised proofs of
As a side product we formalize some properties of Euler's phi-function,
the notion of the order of an element of a group, and the cyclicity of the multiplicative group of a finite field.
notify = noschinl@gmail.com, simon.wimmer@tum.de
[Pratt_Certificate]
title = Pratt's Primality Certificates
author = Simon Wimmer
An article about these proofs is found here.
notify = nipkow@in.tum.de
[SenSocialChoice]
title = Some classical results in Social Choice Theory
author = Peter Gammie
This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.
notify = noschinl@gmail.com
[Planarity_Certificates]
title = Planarity Certificates
author = Lars Noschinski
A matching in a graph G is a subset M of the edges of G such that no two share an endpoint. A matching has maximum cardinality if its cardinality is at least as large as that of any other matching. An odd-set cover OSC of a graph G is a labeling of the nodes of G with integers such that every edge of G is either incident to a node labeled 1 or connects two nodes labeled with the same number i ≥ 2.
This article proves Edmonds theorem:
Let M be a matching in a graph G and let OSC be an
odd-set cover of G.
For any i ≥ 0, let n(i) be the number of nodes
labeled i. If |M| = n(1) +
∑_{i ≥ 2}(n(i) div 2),
then M is a maximum cardinality matching.
This research was supported by the Austrian Science Fund (FWF): J3202.
notify = c.sternagel@gmail.com [Category] title = Category Theory to Yoneda's Lemma author = Greg O'Keefe Compared to traditional proof outlines, ribbon proofs emphasise the structure of a proof, so are intelligible and pedagogical. Because they contain less redundancy than proof outlines, and allow each proof step to be checked locally, they may be more scalable. Where proof outlines are cumbersome to modify, ribbon proofs can be visually manoeuvred to yield proofs of variant programs.
notify =
[Koenigsberg_Friendship]
title = The Königsberg Bridge Problem and the Friendship Theorem
author = Wenda Li
[2018-02-05]: 'Modernized' representation following the formalization in HOL4:
former "float_format" and predicate "is_valid" is now encoded in a type "('e, 'f) float" where
'e and 'f encode the size of exponent and fraction.
[Native_Word]
title = Native Word
author = Andreas Lochbihler
[2014-03-31]:
added words of default size in the target language (by Peter Lammich)
(revision 25caf5065833)
[2014-10-06]:
proper test setup with compilation and execution of tests in all target languages
(revision 5d7a1c9ae047)
[2017-09-02]:
added 64-bit words (revision c89f86244e3c)
[2018-07-15]:
added cast operators for default-size words (revision fc1f1fb8dd30)
notify = mail@andreas-lochbihler.de
[XML]
title = XML
author = Christian Sternagel
[Lowe_Ontological_Argument]
title = Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
author = David Fuenmayor
Tail-recursive function definitions are sometimes more straightforward than alternatives, but proving theorems on them may be roundabout because of the peculiar form of the resulting recursion induction rules.
This paper describes a proof method that provides a general solution to this problem by means of suitable invariants over inductive sets, and illustrates the application of such method by examining two case studies.
notify = pasquale.noce.lavoro@gmail.com [CryptoBasedCompositionalProperties] title = Compositional Properties of Crypto-Based Components author = Maria SpichkovaThis entry provides the definitions and basic properties of the complex and real error function erf and the complementary error function erfc. Additionally, it gives their full asymptotic expansions.
[Akra_Bazzi] title = The Akra-Bazzi theorem and the Master theorem author = Manuel Eberl
Some proof methods that facilitate applying the Master theorem are also
included. For a more detailed explanation of the formalisation and the
proof methods, see the accompanying paper (publication forthcoming).
notify = eberlm@in.tum.de
[Dirichlet_Series]
title = Dirichlet Series
author = Manuel Eberl
This article provides a full formalisation of Chapter 8 of Apostol's Introduction to Analytic Number Theory. Subjects that are covered are:
This entry builds upon the results about formal and analytic Dirichlet series to define the Hurwitz ζ function ζ(a,s) and, based on that, the Riemann ζ function ζ(s). This is done by first defining them for ℜ(z) > 1 and then successively extending the domain to the left using the Euler–MacLaurin formula.
Apart from the most basic facts such as analyticity, the following results are provided:
The entry also contains Euler's analytic proof of the infinitude of primes, based on the fact that ζ(s) has a pole at s = 1.
[Linear_Recurrences] title = Linear Recurrences author = Manuel EberlLinear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n-1) + f(n - 2) and the quite non-obvious closed form (φ^{n} - (-φ)^{-n}) / √5 where φ is the golden ratio.
In this work, I build on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.
[Lambert_W] title = The Lambert W Function on the Reals author = Manuel EberlThe Lambert W function is a multi-valued function defined as the inverse function of x ↦ x e^{x}. Besides numerous applications in combinatorics, physics, and engineering, it also frequently occurs when solving equations containing both e^{x} and x, or both x and log x.
This article provides a definition of the two real-valued branches W_{0}(x) and W_{-1}(x) and proves various properties such as basic identities and inequalities, monotonicity, differentiability, asymptotic expansions, and the MacLaurin series of W_{0}(x) at x = 0.
[Cartan_FP] title = The Cartan Fixed Point Theorems author = Lawrence C. Paulson