metadata 554 KB
Newer Older
Manuel Eberl's avatar
Manuel Eberl committed
1
2
[Arith_Prog_Rel_Primes]
title = Arithmetic progressions and relative primes
3
author = José Manuel Rodríguez Caballero <https://josephcmac.github.io/>
nipkow's avatar
nipkow committed
4
topic = Mathematics/Number theory
Manuel Eberl's avatar
Manuel Eberl committed
5
6
date = 2020-02-01
notify = jose.manuel.rodriguez.caballero@ut.ee
7
abstract =
Manuel Eberl's avatar
Manuel Eberl committed
8
  This article provides a formalization of the solution obtained by the
9
  author of the Problem “ARITHMETIC PROGRESSIONS” from the
Manuel Eberl's avatar
Manuel Eberl committed
10
11
12
13
14
15
  <a href="https://www.ocf.berkeley.edu/~wwu/riddles/putnam.shtml">
  Putnam exam problems of 2002</a>. The statement of the problem is
  as follows: For which integers <em>n</em> > 1 does the set of positive
  integers less than and relatively prime to <em>n</em> constitute an
  arithmetic progression?

16
17
18
19
20
21
22
[Banach_Steinhaus]
title = Banach-Steinhaus Theorem
author = Dominique Unruh <http://kodu.ut.ee/~unruh/> <mailto:unruh@ut.ee>, Jose Manuel Rodriguez Caballero <https://josephcmac.github.io/> <mailto:jose.manuel.rodriguez.caballero@ut.ee>
topic = Mathematics/Analysis
date = 2020-05-02
notify = jose.manuel.rodriguez.caballero@ut.ee, unruh@ut.ee
abstract =
23
24
25
  We formalize in Isabelle/HOL a result
  due to S. Banach and H. Steinhaus known as
  the Banach-Steinhaus theorem or Uniform boundedness principle: a
26
27
  pointwise-bounded family of continuous linear operators from a Banach
  space to a normed space is uniformly bounded. Our approach is an
28
  adaptation to Isabelle/HOL of a proof due to A. Sokal.
29

30
31
32
33
34
35
[Complex_Geometry]
title = Complex Geometry
author = Filip Marić <http://www.matf.bg.ac.rs/~filip>, Danijela Simić <http://poincare.matf.bg.ac.rs/~danijela>
topic = Mathematics/Geometry
date = 2019-12-16
notify = danijela@matf.bg.ac.rs, filip@matf.bg.ac.rs, boutry@unistra.fr
Lawrence Paulson's avatar
Lawrence Paulson committed
36
abstract =
37
38
39
40
41
42
43
44
45
46
47
48
49
50
  A formalization of geometry of complex numbers is presented.
  Fundamental objects that are investigated are the complex plane
  extended by a single infinite point, its objects (points, lines and
  circles), and groups of transformations that act on them (e.g.,
  inversions and Möbius transformations). Most objects are defined
  algebraically, but correspondence with classical geometric definitions
  is shown.

[Poincare_Disc]
title = Poincaré Disc Model
author = Danijela Simić <http://poincare.matf.bg.ac.rs/~danijela>,  Filip Marić <http://www.matf.bg.ac.rs/~filip>,  Pierre Boutry <mailto:boutry@unistra.fr>
topic = Mathematics/Geometry
date = 2019-12-16
notify = danijela@matf.bg.ac.rs, filip@matf.bg.ac.rs, boutry@unistra.fr
Lawrence Paulson's avatar
Lawrence Paulson committed
51
abstract =
52
53
54
  We describe formalization of the Poincaré disc model of hyperbolic
  geometry within the Isabelle/HOL proof assistant. The model is defined
  within the extended complex plane (one dimensional complex projectives
55
  space &#8450;P1), formalized in the AFP entry “Complex Geometry”.
56
57
58
59
60
61
62
  Points, lines, congruence of pairs of points, betweenness of triples
  of points, circles, and isometries are defined within the model. It is
  shown that the model satisfies all Tarski's axioms except the
  Euclid's axiom. It is shown that it satisfies its negation and
  the limiting parallels axiom (which proves it to be a model of
  hyperbolic geometry).

nipkow's avatar
nipkow committed
63
64
65
66
67
68
[Fourier]
title = Fourier Series
author = Lawrence C Paulson <https://www.cl.cam.ac.uk/~lp15/>
topic = Mathematics/Analysis
date = 2019-09-06
notify = lp15@cam.ac.uk
Lawrence Paulson's avatar
Lawrence Paulson committed
69
abstract =
nipkow's avatar
nipkow committed
70
71
72
73
74
75
  This development formalises the square integrable functions over the
  reals and the basics of Fourier series. It culminates with a proof
  that every well-behaved periodic function can be approximated by a
  Fourier series. The material is ported from HOL Light:
  https://github.com/jrh13/hol-light/blob/master/100/fourier.ml

Gerwin Klein's avatar
Gerwin Klein committed
76
77
78
[Generic_Deriving]
title = Deriving generic class instances for datatypes
author = Jonas Rädle <mailto:jonas.raedle@gmail.com>, Lars Hupel <https://www21.in.tum.de/~hupel/>
nipkow's avatar
nipkow committed
79
topic = Computer science/Data structures
Gerwin Klein's avatar
Gerwin Klein committed
80
81
82
83
84
85
86
87
88
89
90
91
92
93
date = 2018-11-06
notify = jonas.raedle@gmail.com
abstract =
  <p>We provide a framework for automatically deriving instances for
  generic type classes. Our approach is inspired by Haskell's
  <i>generic-deriving</i> package and Scala's
  <i>shapeless</i> 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.</p>
  <p>Note: There are already articles in the AFP that provide
   automatic instantiation for a number of classes. Concretely, <a href="https://www.isa-afp.org/entries/Deriving.html">Deriving</a> allows the automatic instantiation of comparators, linear orders, equality, and hashing. <a href="https://www.isa-afp.org/entries/Show.html">Show</a> instantiates a Haskell-style <i>show</i> class.</p><p>Our approach works for arbitrary classes (with some Isabelle/HOL overhead for each class), but a smaller set of datatypes.</p>


94
95
96
[Partial_Order_Reduction]
title = Partial Order Reduction
author = Julian Brunner <http://www21.in.tum.de/~brunnerj/>
nipkow's avatar
nipkow committed
97
topic = Computer science/Automata and formal languages
98
99
date = 2018-06-05
notify = brunnerj@in.tum.de
100
abstract =
101
102
103
104
105
106
107
  This entry provides a formalization of the abstract theory of ample
  set partial order reduction. The formalization includes transition
  systems with actions, trace theory, as well as basics on finite,
  infinite, and lazy sequences. We also provide a basic framework for
  static analysis on concurrent systems with respect to the ample set
  condition.

108
109
[CakeML]
title = CakeML
Lars Hupel's avatar
Lars Hupel committed
110
author = Lars Hupel <https://www21.in.tum.de/~hupel/>, Yu Zhang <>
111
contributors = Johannes Åman Pohjola <>
nipkow's avatar
nipkow committed
112
topic = Computer science/Programming languages/Language definitions
113
114
date = 2018-03-12
notify = hupel@in.tum.de
Lars Hupel's avatar
Lars Hupel committed
115
abstract =
116
117
118
119
120
121
122
  CakeML is a functional programming language with a proven-correct
  compiler and runtime system. This entry contains an unofficial version
  of the CakeML semantics that has been exported from the Lem
  specifications to Isabelle. Additionally, there are some hand-written
  theory files that adapt the exported code to Isabelle and port proofs
  from the HOL4 formalization, e.g. termination and equivalence proofs.

Lawrence Paulson's avatar
Lawrence Paulson committed
123
124
125
[CakeML_Codegen]
title = A Verified Code Generator from Isabelle/HOL to CakeML
author = Lars Hupel <https://lars.hupel.info/>
nipkow's avatar
nipkow committed
126
topic = Computer science/Programming languages/Compiling, Logic/Rewriting
Lawrence Paulson's avatar
Lawrence Paulson committed
127
128
129
130
131
132
133
134
135
136
date = 2019-07-08
notify = lars@hupel.info
abstract =
  This entry contains the formalization that accompanies my PhD thesis
  (see https://lars.hupel.info/research/codegen/). I develop a verified
  compilation toolchain from executable specifications in Isabelle/HOL
  to CakeML abstract syntax trees. This improves over the
  state-of-the-art in Isabelle by providing a trustworthy procedure for
  code generation.

137
138
139
[DiscretePricing]
title = Pricing in discrete financial models
author = Mnacho Echenim <http://lig-membres.imag.fr/mechenim/>
nipkow's avatar
nipkow committed
140
topic = Mathematics/Probability theory, Mathematics/Games and economics
141
142
143
144
145
146
147
148
149
date = 2018-07-16
notify = mnacho.echenim@univ-grenoble-alpes.fr
abstract =
  We have formalized the computation of fair prices for derivative
  products in discrete financial models. As an application, we derive a
  way to compute fair prices of derivative products in the
  Cox-Ross-Rubinstein model of a financial market, thus completing the
  work that was presented in this <a
  href="https://hal.archives-ouvertes.fr/hal-01562944">paper</a>.
mechenim's avatar
mechenim committed
150
151
152
153
154
155
156
157
158
extra-history =
	Change history:
	[2019-05-12]:
	Renamed discr_mkt predicate to stk_strict_subs and got rid of predicate A for a more natural definition of the type discrete_market;
    renamed basic quantity processes for coherent notation;
    renamed value_process into val_process and closing_value_process to cls_val_process;
    relaxed hypothesis of lemma CRR_market_fair_price.
    Added functions to price some basic options.
	(revision 0b813a1a833f)<br>
kleing's avatar
kleing committed
159

160

gerwin.klein@data61.csiro.au's avatar
gerwin.klein@data61.csiro.au committed
161
162
163
[Pell]
title = Pell's Equation
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
164
topic = Mathematics/Number theory
gerwin.klein@data61.csiro.au's avatar
gerwin.klein@data61.csiro.au committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
date = 2018-06-23
notify = eberlm@in.tum.de
abstract =
  <p> This article gives the basic theory of Pell's equation
  <em>x</em><sup>2</sup> = 1 +
  <em>D</em>&thinsp;<em>y</em><sup>2</sup>,
  where
  <em>D</em>&thinsp;&isin;&thinsp;&#8469; is
  a parameter and <em>x</em>, <em>y</em> are
  integer variables. </p> <p> The main result that is proven
  is the following: If <em>D</em> is not a perfect square,
  then there exists a <em>fundamental solution</em>
  (<em>x</em><sub>0</sub>,
  <em>y</em><sub>0</sub>) that is not the
  trivial solution (1, 0) and which generates all other solutions
  (<em>x</em>, <em>y</em>) in the sense that
  there exists some
  <em>n</em>&thinsp;&isin;&thinsp;&#8469;
  such that |<em>x</em>| +
  |<em>y</em>|&thinsp;&radic;<span
  style="text-decoration:
  overline"><em>D</em></span> =
  (<em>x</em><sub>0</sub> +
  <em>y</em><sub>0</sub>&thinsp;&radic;<span
  style="text-decoration:
  overline"><em>D</em></span>)<sup><em>n</em></sup>.
  This also implies that the set of solutions is infinite, and it gives
  us an explicit and executable characterisation of all the solutions.
  </p> <p> Based on this, simple executable algorithms for
  computing the fundamental solution and the infinite sequence of all
  non-negative solutions are also provided. </p>

nipkow's avatar
nipkow committed
197
198
199
[WebAssembly]
title = WebAssembly
author = Conrad Watt <http://www.cl.cam.ac.uk/~caw77/>
nipkow's avatar
nipkow committed
200
topic = Computer science/Programming languages/Language definitions
nipkow's avatar
nipkow committed
201
202
date = 2018-04-29
notify = caw77@cam.ac.uk
Lawrence Paulson's avatar
Lawrence Paulson committed
203
abstract =
nipkow's avatar
nipkow committed
204
205
206
207
208
209
210
  This is a mechanised specification of the WebAssembly language, drawn
  mainly from the previously published paper formalisation of Haas et
  al. Also included is a full proof of soundness of the type system,
  together with a verified type checker and interpreter. We include only
  a partial procedure for the extraction of the type checker and
  interpreter here. For more details, please see our paper in CPP 2018.

nipkow's avatar
nipkow committed
211
212
[Knuth_Morris_Pratt]
title = The string search algorithm by Knuth, Morris and Pratt
213
author = Fabian Hellauer <mailto:hellauer@in.tum.de>, Peter Lammich <http://www21.in.tum.de/~lammich>
nipkow's avatar
nipkow committed
214
topic = Computer science/Algorithms
nipkow's avatar
nipkow committed
215
216
date = 2017-12-18
notify = hellauer@in.tum.de, lammich@in.tum.de
217
abstract =
nipkow's avatar
nipkow committed
218
  The Knuth-Morris-Pratt algorithm is often used to show that the
nipkow's avatar
nipkow committed
219
220
221
  problem of finding a string <i>s</i> in a text
  <i>t</i> can be solved deterministically in
  <i>O(|s| + |t|)</i> time. We use the Isabelle
nipkow's avatar
nipkow committed
222
223
224
225
226
  Refinement Framework to formulate and verify the algorithm. Via
  refinement, we apply some optimisations and finally use the
  <em>Sepref</em> tool to obtain executable code in
  <em>Imperative/HOL</em>.

227
228
229
[Minkowskis_Theorem]
title = Minkowski's Theorem
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
230
topic = Mathematics/Geometry, Mathematics/Number theory
231
232
date = 2017-07-13
notify = eberlm@in.tum.de
233
abstract =
234
235
236
237
238
239
240
241
242
243
244
245
246
247
  <p>Minkowski's theorem relates a subset of
  &#8477;<sup>n</sup>, the Lebesgue measure, and the
  integer lattice &#8484;<sup>n</sup>: It states that
  any convex subset of &#8477;<sup>n</sup> with volume
  greater than 2<sup>n</sup> contains at least one lattice
  point from &#8484;<sup>n</sup>\{0}, i.&thinsp;e. a
  non-zero point with integer coefficients.</p>  <p>A
  related theorem which directly implies this is Blichfeldt's
  theorem, which states that any subset of
  &#8477;<sup>n</sup> with a volume greater than 1
  contains two different points whose difference vector has integer
  components.</p>  <p>The entry contains a proof of both
  theorems.</p>

248
249
250
[Name_Carrying_Type_Inference]
title = Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
author = Michael Rawson <mailto:michaelrawson76@gmail.com>
nipkow's avatar
nipkow committed
251
topic = Computer science/Programming languages/Type systems
252
253
date = 2017-07-09
notify = mr644@cam.ac.uk, michaelrawson76@gmail.com
254
abstract =
255
256
257
258
259
260
261
262
263
264
265
  I formalise a Church-style simply-typed
  \(\lambda\)-calculus, extended with pairs, a unit value, and
  projection functions, and show some metatheory of the calculus, such
  as the subject reduction property. Particular attention is paid to the
  treatment of names in the calculus. A nominal style of binding is
  used, but I use a manual approach over Nominal Isabelle in order to
  extract an executable type inference algorithm. More information can
  be found in my <a
  href="http://www.openthesis.org/documents/Verified-Metatheory-Type-Inference-Simply-603182.html">undergraduate
  dissertation</a>.

Rene Thiemann's avatar
Rene Thiemann committed
266
267
[Propositional_Proof_Systems]
title = Propositional Proof Systems
268
author = Julius Michaelis <http://liftm.de>, Tobias Nipkow <http://www21.in.tum.de/~nipkow>
nipkow's avatar
nipkow committed
269
topic = Logic/Proof theory
Rene Thiemann's avatar
Rene Thiemann committed
270
271
date = 2017-06-21
notify = maintainafpppt@liftm.de
272
abstract =
Rene Thiemann's avatar
Rene Thiemann committed
273
274
275
276
277
278
279
  We formalize a range of proof systems for classical propositional
  logic (sequent calculus, natural deduction, Hilbert systems,
  resolution) and prove the most important meta-theoretic results about
  semantics and proofs: compactness, soundness, completeness,
  translations between proof systems, cut-elimination, interpolation and
  model existence.

280
281
282
[Optics]
title = Optics
author = Simon Foster <mailto:simon.foster@york.ac.uk>, Frank Zeyda <mailto:frank.zeyda@york.ac.uk>
nipkow's avatar
nipkow committed
283
topic = Computer science/Functional programming, Mathematics/Algebra
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
date = 2017-05-25
notify = simon.foster@york.ac.uk
abstract =
  Lenses provide an abstract interface for manipulating data types
  through spatially-separated views. They are defined abstractly in
  terms of two functions, <em>get</em>, the return a value
  from the source type, and <em>put</em> that updates the
  value. We mechanise the underlying theory of lenses, in terms of an
  algebraic hierarchy of lenses, including well-behaved and very
  well-behaved lenses, each lens class being characterised by a set of
  lens laws. We also mechanise a lens algebra in Isabelle that enables
  their composition and comparison, so as to allow construction of
  complex lenses. This is accompanied by a large library of algebraic
  laws. Moreover we also show how the lens classes can be applied by
  instantiating them with a number of Isabelle data types.
299
300
301
302
303
304
305
306
extra-history =
	Change history:
	[2020-03-02]:
	Added partial bijective and symmetric lenses.
        Improved alphabet command generating additional lenses and results.
        Several additional lens relations, including observational equivalence.
        Additional theorems throughout.
        Adaptations for Isabelle 2020.
Gerwin Klein's avatar
Gerwin Klein committed
307
        (revision 44e2e5c)
308

Rene Thiemann's avatar
Rene Thiemann committed
309
310
[Game_Based_Crypto]
title = Game-based cryptography in HOL
311
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>, S. Reza Sefidgar <>, Bhargav Bhatt <mailto:bhargav.bhatt@inf.ethz.ch>
nipkow's avatar
nipkow committed
312
topic = Computer science/Security/Cryptography
Rene Thiemann's avatar
Rene Thiemann committed
313
date = 2017-05-05
314
notify = mail@andreas-lochbihler.de
315
abstract =
Rene Thiemann's avatar
Rene Thiemann committed
316
317
318
319
320
321
322
323
324
  <p>In 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
325
  functions.
Rene Thiemann's avatar
Rene Thiemann committed
326
327
328
329
330
331
  </p><p>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.</p>
Andreas Lochbihler's avatar
Andreas Lochbihler committed
332
333
334
335
336
extra-history =
	Change history:
	[2018-09-28]:
	added the CryptHOL tutorial for game-based cryptography
	(revision 489a395764ae)
Rene Thiemann's avatar
Rene Thiemann committed
337

338
339
340
[Multi_Party_Computation]
title = Multi-Party Computation
author = David Aspinall <http://homepages.inf.ed.ac.uk/da/>, David Butler <mailto:dbutler@turing.ac.uk>
nipkow's avatar
nipkow committed
341
topic = Computer science/Security
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
date = 2019-05-09
notify = dbutler@turing.ac.uk
abstract =
  We use CryptHOL to consider Multi-Party Computation (MPC) protocols.
  MPC was first considered by Yao in 1983 and recent advances in
  efficiency and an increased demand mean it is now deployed in the real
  world. Security is considered using the real/ideal world paradigm. We
  first define security in the semi-honest security setting where
  parties are assumed not to deviate from the protocol transcript. In
  this setting we prove multiple Oblivious Transfer (OT) protocols
  secure and then show security for the gates of the GMW protocol. We
  then define malicious security, this is a stronger notion of security
  where parties are assumed to be fully corrupted by an adversary. In
  this setting we again consider OT, as it is a fundamental building
  block of almost all MPC protocols.

Lawrence Paulson's avatar
Lawrence Paulson committed
358
359
360
[Sigma_Commit_Crypto]
title = Sigma Protocols and Commitment Schemes
author = David Butler <https://www.turing.ac.uk/people/doctoral-students/david-butler>, Andreas Lochbihler <http://www.andreas-lochbihler.de>
nipkow's avatar
nipkow committed
361
topic = Computer science/Security/Cryptography
Lawrence Paulson's avatar
Lawrence Paulson committed
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
date = 2019-10-07
notify = dbutler@turing.ac.uk
abstract =
  We use CryptHOL to formalise commitment schemes and Sigma-protocols.
  Both are widely used fundamental two party cryptographic primitives.
  Security for commitment schemes is considered using game-based
  definitions whereas the security of Sigma-protocols is considered
  using both the game-based and simulation-based security paradigms. In
  this work, we first define security for both primitives and then prove
  secure multiple case studies: the Schnorr, Chaum-Pedersen and
  Okamoto Sigma-protocols as well as a construction that allows for
  compound (AND and OR statements) Sigma-protocols and the Pedersen and
  Rivest commitment schemes. We also prove that commitment schemes can
  be constructed from Sigma-protocols. We formalise this proof at an
  abstract level, only assuming the existence of a Sigma-protocol;
  consequently, the instantiations of this result for the concrete
  Sigma-protocols we consider come for free.

Rene Thiemann's avatar
Rene Thiemann committed
380
381
[CryptHOL]
title = CryptHOL
382
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>
nipkow's avatar
nipkow committed
383
topic = Computer science/Security/Cryptography, Computer science/Functional programming, Mathematics/Probability theory
Rene Thiemann's avatar
Rene Thiemann committed
384
date = 2017-05-05
385
notify = mail@andreas-lochbihler.de
386
abstract =
Rene Thiemann's avatar
Rene Thiemann committed
387
388
  <p>CryptHOL provides a framework for formalising cryptographic arguments
  in Isabelle/HOL. It shallowly embeds a probabilistic functional
389
  programming language in higher order logic. The language features
Rene Thiemann's avatar
Rene Thiemann committed
390
391
  monadic sequencing, recursion, random sampling, failures and failure
  handling, and black-box access to oracles. Oracles are probabilistic
392
  functions which maintain hidden state between different invocations.
Rene Thiemann's avatar
Rene Thiemann committed
393
394
395
396
  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
397
  comprehensible, and the framework is extensible and widely applicable.
Rene Thiemann's avatar
Rene Thiemann committed
398
399
400
401
402
  </p><p>
  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.</p>
403

404
405
[Constructive_Cryptography]
title = Constructive Cryptography in HOL
nipkow's avatar
nipkow committed
406
author = Andreas Lochbihler <http://www.andreas-lochbihler.de/>, S. Reza Sefidgar<>
nipkow's avatar
nipkow committed
407
topic = Computer science/Security/Cryptography, Mathematics/Probability theory
408
409
410
411
412
413
414
415
416
417
418
419
420
421
date = 2018-12-17
notify = mail@andreas-lochbihler.de, reza.sefidgar@inf.ethz.ch
abstract =
  Inspired by Abstract Cryptography, we extend CryptHOL, a framework for
  formalizing game-based proofs, with an abstract model of Random
  Systems and provide proof rules about their composition and equality.
  This foundation facilitates the formalization of Constructive
  Cryptography proofs, where the security of a cryptographic scheme is
  realized as a special form of construction in which a complex random
  system is built from simpler ones. This is a first step towards a
  fully-featured compositional framework, similar to Universal
  Composability framework, that supports formalization of
  simulation-based proofs.

422
423
[Probabilistic_While]
title = Probabilistic while loop
424
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>
nipkow's avatar
nipkow committed
425
topic = Computer science/Functional programming, Mathematics/Probability theory, Computer science/Algorithms
426
date = 2017-05-05
427
notify = mail@andreas-lochbihler.de
428
429
abstract =
  This AFP entry defines a probabilistic while operator based on
430
431
432
433
434
  sub-probability mass functions and formalises zero-one laws and variant
  rules for probabilistic loop termination. As applications, we
  implement probabilistic algorithms for the Bernoulli, geometric and
  arbitrary uniform distributions that only use fair coin flips, and
  prove them correct and terminating with probability 1.
Andreas Lochbihler's avatar
Andreas Lochbihler committed
435
436
437
438
439
440
extra-history =
	Change history:
	[2018-02-02]:
	Added a proof that probabilistic conditioning can be implemented by repeated sampling.
	(revision 305867c4e911)<br>

441

442
443
[Monad_Normalisation]
title = Monad normalisation
444
author = Joshua Schneider <>, Manuel Eberl <https://www21.in.tum.de/~eberlm>, Andreas Lochbihler <http://www.andreas-lochbihler.de>
nipkow's avatar
nipkow committed
445
topic = Tools, Computer science/Functional programming, Logic/Rewriting
446
date = 2017-05-05
447
notify = mail@andreas-lochbihler.de
448
abstract =
449
  The usual monad laws can directly be used as rewrite rules for Isabelle’s
450
  simplifier to normalise monadic HOL terms and decide equivalences.
451
  In a commutative monad, however, the commutativity law is a
452
453
  higher-order permutative rewrite rule that makes the simplifier loop.
  This AFP entry implements a simproc that normalises monadic
454
  expressions in commutative monads using ordered rewriting. The
455
  simproc can also permute computations across control operators like if
456
  and case.
457

458
459
[Monomorphic_Monad]
title = Effect polymorphism in higher-order logic
460
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>
nipkow's avatar
nipkow committed
461
topic = Computer science/Functional programming
462
date = 2017-05-05
463
notify = mail@andreas-lochbihler.de
464
abstract =
465
466
467
468
469
470
471
472
473
  The notion of a monad cannot be expressed within higher-order logic
  (HOL) due to type system restrictions. We show that if a monad is used
  with values of only one type, this notion can be formalised in HOL.
  Based on this idea, we develop a library of effect specifications and
  implementations of monads and monad transformers. Hence, we can
  abstract over the concrete monad in HOL definitions and thus use the
  same definition for different (combinations of) effects. We illustrate
  the usefulness of effect polymorphism with a monadic interpreter for a
  simple language.
Andreas Lochbihler's avatar
Andreas Lochbihler committed
474
475
476
477
478
479
480
extra-history =
	Change history:
	[2018-02-15]:
	added further specifications and implementations of non-determinism;
        more examples
	(revision bc5399eea78e)<br>

481

Rene Thiemann's avatar
Rene Thiemann committed
482
483
484
485
486
487
[Constructor_Funs]
title = Constructor Functions
author = Lars Hupel <https://www21.in.tum.de/~hupel/>
topic = Tools
date = 2017-04-19
notify = hupel@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
488
abstract =
Rene Thiemann's avatar
Rene Thiemann committed
489
490
491
492
493
494
495
  Isabelle's code generator performs various adaptations for target
  languages. Among others, constructor applications have to be fully
  saturated. That means that for constructor calls occuring as arguments
  to higher-order functions, synthetic lambdas have to be inserted. This
  entry provides tooling to avoid this construction altogether by
  introducing constructor functions.

Rene Thiemann's avatar
Rene Thiemann committed
496
497
498
499
500
501
[Lazy_Case]
title = Lazifying case constants
author = Lars Hupel <https://www21.in.tum.de/~hupel/>
topic = Tools
date = 2017-04-18
notify = hupel@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
502
abstract =
Rene Thiemann's avatar
Rene Thiemann committed
503
504
505
506
507
508
509
510
511
512
513
514
515
  Isabelle's code generator performs various adaptations for target
  languages. Among others, case statements are printed as match
  expressions. Internally, this is a sophisticated procedure, because in
  HOL, case statements are represented as nested calls to the case
  combinators as generated by the datatype package. Furthermore, the
  procedure relies on laziness of match expressions in the target
  language, i.e., that branches guarded by patterns that fail to match
  are not evaluated. Similarly, <tt>if-then-else</tt> is
  printed to the corresponding construct in the target language. This
  entry provides tooling to replace these special cases in the code
  generator by ignoring these target language features, instead printing
  case expressions and <tt>if-then-else</tt> as functions.

516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
[Dict_Construction]
title = Dictionary Construction
author = Lars Hupel <https://www21.in.tum.de/~hupel/>
topic = Tools
date = 2017-05-24
notify = hupel@in.tum.de
abstract =
  Isabelle's code generator natively supports type classes. For
  targets that do not have language support for classes and instances,
  it performs the well-known dictionary translation, as described by
  Haftmann and Nipkow. This translation happens outside the logic, i.e.,
  there is no guarantee that it is correct, besides the pen-and-paper
  proof. This work implements a certified dictionary translation that
  produces new class-free constants and derives equality theorems.

531
532
533
[Higher_Order_Terms]
title = An Algebra for Higher-Order Terms
author = Lars Hupel <https://lars.hupel.info/>
534
contributors = Yu Zhang <>
nipkow's avatar
nipkow committed
535
topic = Computer science/Programming languages/Lambda calculi
536
537
538
539
540
541
542
543
date = 2019-01-15
notify = lars@hupel.info
abstract =
  In this formalization, I introduce a higher-order term algebra,
  generalizing the notions of free variables, matching, and
  substitution. The need arose from the work on a <a
  href="http://dx.doi.org/10.1007/978-3-319-89884-1_35">verified
  compiler from Isabelle to CakeML</a>. Terms can be thought of as
544
  consisting of a generic (free variables, constants, application) and
545
546
547
548
549
550
551
552
  a specific part. As example applications, this entry provides
  instantiations for de-Bruijn terms, terms with named variables, and
  <a
  href="https://www.isa-afp.org/entries/Lambda_Free_RPOs.html">Blanchette’s
  &lambda;-free higher-order terms</a>. Furthermore, I
  implement translation functions between de-Bruijn terms and named
  terms and prove their correctness.

kleing's avatar
kleing committed
553
554
555
556
557
558
[Subresultants]
title = Subresultants
author = Sebastiaan Joosten <mailto:sebastiaan.joosten@uibk.ac.at>, René Thiemann <mailto:rene.thiemann@uibk.ac.at>, Akihisa Yamada <mailto:akihisa.yamada@uibk.ac.at>
topic = Mathematics/Algebra
date = 2017-04-06
notify = rene.thiemann@uibk.ac.at
Lawrence Paulson's avatar
Lawrence Paulson committed
559
abstract =
kleing's avatar
kleing committed
560
561
562
563
564
  We formalize the theory of subresultants and the subresultant
  polynomial remainder sequence as described by Brown and Traub. As a
  result, we obtain efficient certified algorithms for computing the
  resultant and the greatest common divisor of polynomials.

565
566
567
[Comparison_Sort_Lower_Bound]
title = Lower bound on comparison-based sorting algorithms
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
568
topic = Computer science/Algorithms
569
570
date = 2017-03-15
notify = eberlm@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
571
abstract =
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
  <p>This 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 <em>n</em> is at
  least <em>log<sub>2</sub>&nbsp;(n!)</em>
  in the worst case, i.&thinsp;e.&nbsp;<em>Ω(n log
  n)</em>.</p>  <p>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.</p>

[Quick_Sort_Cost]
title = The number of comparisons in QuickSort
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
588
topic = Computer science/Algorithms
589
590
date = 2017-03-15
notify = eberlm@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
591
abstract =
592
593
594
595
596
597
598
599
600
601
  <p>We 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.&thinsp;e.&nbsp;QuickSort with random pivot choice) is
  <em>2&thinsp;(n+1)&thinsp;H<sub>n</sub> -
  4&thinsp;n</em>, which is asymptotically equivalent to
  <em>2&thinsp;n ln n</em>; second, the number of
  comparisons performed by the classic non-randomised QuickSort has the
  same distribution in the average case as the randomised one.</p>

nipkow's avatar
nipkow committed
602
603
604
[Random_BSTs]
title = Expected Shape of Random Binary Search Trees
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
605
topic = Computer science/Data structures
nipkow's avatar
nipkow committed
606
607
date = 2017-04-04
notify = eberlm@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
608
abstract =
nipkow's avatar
nipkow committed
609
610
611
612
613
614
615
616
617
618
  <p>This entry contains proofs for the textbook results about the
  distributions of the height and internal path length of random binary
  search trees (BSTs), i.&thinsp;e. BSTs that are formed by taking
  an empty BST and inserting elements from a fixed set in random
  order.</p>  <p>In particular, we prove a logarithmic upper
  bound on the expected height and the <em>Θ(n log n)</em>
  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.</p>

Lawrence Paulson's avatar
Lawrence Paulson committed
619
620
621
[Randomised_BSTs]
title = Randomised Binary Search Trees
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
622
topic = Computer science/Data structures
Lawrence Paulson's avatar
Lawrence Paulson committed
623
624
625
626
627
628
629
630
631
632
633
date = 2018-10-19
notify = eberlm@in.tum.de
abstract =
  <p>This work is a formalisation of the Randomised Binary Search
  Trees introduced by Martínez and Roura, including definitions and
  correctness proofs.</p> <p>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.</p>

Gerwin Klein's avatar
Gerwin Klein committed
634
635
636
[E_Transcendental]
title = The Transcendence of e
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
637
topic = Mathematics/Analysis, Mathematics/Number theory
Gerwin Klein's avatar
Gerwin Klein committed
638
639
date = 2017-01-12
notify = eberlm@in.tum.de
Lawrence Paulson's avatar
Lawrence Paulson committed
640
abstract =
Gerwin Klein's avatar
Gerwin Klein committed
641
642
643
644
645
646
  <p>This 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.</p> <p>This kind of approach can be found in
  many different sources; this formalisation mostly follows a <a  href="http://planetmath.org/proofoflindemannweierstrasstheoremandthateandpiaretranscendental">PlanetMath article</a> by Roger Lipsett.</p>

Lawrence Paulson's avatar
Lawrence Paulson committed
647
648
649
[Pi_Transcendental]
title = The Transcendence of π
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
nipkow's avatar
nipkow committed
650
topic = Mathematics/Number theory
Lawrence Paulson's avatar
Lawrence Paulson committed
651
652
653
654
655
656
657
658
659
660
date = 2018-09-28
notify = eberlm@in.tum.de
abstract =
  <p>This entry shows the transcendence of &pi; 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
  <em>e</em>.</p>

661
662
[DFS_Framework]
title = A Framework for Verifying Depth-First Search Algorithms
663
author = Peter Lammich <http://www21.in.tum.de/~lammich>, René Neumann <mailto:neumannr@in.tum.de>
664
665
notify = lammich@in.tum.de
date = 2016-07-05
nipkow's avatar
nipkow committed
666
topic = Computer science/Algorithms/Graph
Lawrence Paulson's avatar
Lawrence Paulson committed
667
abstract =
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
	<p>
	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.
	</p><p>
	[CPP-2015] Peter Lammich, René Neumann: A Framework for Verifying
	Depth-First Search Algorithms. CPP 2015: 137-146</p>
684

Lawrence Paulson's avatar
Lawrence Paulson committed
685
686
[Flow_Networks]
title = Flow Networks and the Min-Cut-Max-Flow Theorem
687
author = Peter Lammich <http://www21.in.tum.de/~lammich>, S. Reza Sefidgar <>
nipkow's avatar
nipkow committed
688
topic = Mathematics/Graph theory
Lawrence Paulson's avatar
Lawrence Paulson committed
689
690
691
692
693
date = 2017-06-01
notify = lammich@in.tum.de
abstract =
  We present a formalization of flow networks and the Min-Cut-Max-Flow
  theorem. Our formal proof closely follows a standard textbook proof,
Lawrence Paulson's avatar
Lawrence Paulson committed
694
  and is accessible even without being an expert in Isabelle/HOL, the
Lawrence Paulson's avatar
Lawrence Paulson committed
695
696
  interactive theorem prover used for the formalization.

Lawrence Paulson's avatar
Lawrence Paulson committed
697
698
[Prpu_Maxflow]
title = Formalizing Push-Relabel Algorithms
699
author = Peter Lammich <http://www21.in.tum.de/~lammich>, S. Reza Sefidgar <>
nipkow's avatar
nipkow committed
700
topic = Computer science/Algorithms/Graph, Mathematics/Graph theory
Lawrence Paulson's avatar
Lawrence Paulson committed
701
702
703
704
705
706
707
708
709
710
711
712
713
714
date = 2017-06-01
notify = lammich@in.tum.de
abstract =
  We present a formalization of push-relabel algorithms for computing
  the maximum flow in a network. We start with Goldberg's et
  al.~generic push-relabel algorithm, for which we show correctness and
  the time complexity bound of O(V^2E). We then derive the
  relabel-to-front and FIFO implementation. Using stepwise refinement
  techniques, we derive an efficient verified implementation.  Our
  formal proof of the abstract algorithms closely follows a standard
  textbook proof. It is accessible even without being an expert in
  Isabelle/HOL, the interactive theorem prover used for the
  formalization.

715
716
717
718
719
720
[Buildings]
title = Chamber Complexes, Coxeter Systems, and Buildings
author = Jeremy Sylvestre <http://ualberta.ca/~jsylvest/>
notify = jeremy.sylvestre@ualberta.ca
date = 2016-07-01
topic = Mathematics/Algebra, Mathematics/Geometry
Lawrence Paulson's avatar
Lawrence Paulson committed
721
abstract =
722
723
724
725
726
727
728
729
730
731
	We provide a basic formal framework for the theory of chamber
	complexes and Coxeter systems, and for buildings as thick chamber
	complexes endowed with a system of apartments. Along the way, we
	develop some of the general theory of abstract simplicial complexes
	and of groups (relying on the <i>group_add</i> class for the basics),
	including free groups and group presentations, and their universal
	properties. The main results verified are that the deletion condition
	is both necessary and sufficient for a group with a set of generators
	of order two to be a Coxeter system, and that the apartments in a
	(thick) building are all uniformly Coxeter.
732

733
734
735
736
737
738
[Algebraic_VCs]
title = Program Construction and Verification Components Based on Kleene Algebra
author = Victor B. F. Gomes <mailto:victor.gomes@cl.cam.ac.uk>, Georg Struth <mailto:g.struth@sheffield.ac.uk>
notify = victor.gomes@cl.cam.ac.uk, g.struth@sheffield.ac.uk
date = 2016-06-18
topic = Mathematics/Algebra
Lawrence Paulson's avatar
Lawrence Paulson committed
739
abstract =
740
741
742
743
744
745
746
747
748
749
750
751
	Variants of Kleene algebra support program construction and
	verification by algebraic reasoning. This entry provides a
	verification component for Hoare logic based on Kleene algebra with
	tests, verification components for weakest preconditions and strongest
	postconditions based on Kleene algebra with domain and a component for
	step-wise refinement based on refinement Kleene algebra with tests. In
	addition to these components for the partial correctness of while
	programs, a verification component for total correctness based on
	divergence Kleene algebras and one for (partial correctness) of
	recursive programs based on domain quantales are provided. Finally we
	have integrated memory models for programs with pointers and a program
	trace semantics into the weakest precondition component.
752

753
754
755
[C2KA_DistributedSystems]
title = Communicating Concurrent Kleene Algebra for Distributed Systems Specification
author = Maxime Buyse <mailto:maxime.buyse@polytechnique.edu>, Jason Jaskolka <https://carleton.ca/jaskolka/>
nipkow's avatar
nipkow committed
756
topic = Computer science/Automata and formal languages, Mathematics/Algebra
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
date = 2019-08-06
notify = maxime.buyse@polytechnique.edu, jason.jaskolka@carleton.ca
abstract =
  Communicating Concurrent Kleene Algebra (C²KA) is a mathematical
  framework for capturing the communicating and concurrent behaviour of
  agents in distributed systems. It extends Hoare et al.'s
  Concurrent Kleene Algebra (CKA) with communication actions through the
  notions of stimuli and shared environments. C²KA has applications in
  studying system-level properties of distributed systems such as
  safety, security, and reliability. In this work, we formalize results
  about C²KA and its application for distributed systems specification.
  We first formalize the stimulus structure and behaviour structure
  (CKA). Next, we combine them to formalize C²KA and its properties.
  Then, we formalize notions and properties related to the topology of
  distributed systems and the potential for communication via stimuli
  and via shared environments of agents, all within the algebraic
  setting of C²KA.

775
776
777
778
779
780
[Card_Equiv_Relations]
title = Cardinality of Equivalence Relations
author = Lukas Bulwahn <mailto:lukas.bulwahn@gmail.com>
notify = lukas.bulwahn@gmail.com
date = 2016-05-24
topic = Mathematics/Combinatorics
Lawrence Paulson's avatar
Lawrence Paulson committed
781
abstract =
782
783
784
785
786
787
788
789
790
791
792
793
794
	This entry provides formulae for counting the number of equivalence
	relations and partial equivalence relations over a finite carrier set
	with given cardinality.  To count the number of equivalence relations,
	we provide bijections between equivalence relations and set
	partitions, and then transfer the main results of the two AFP entries,
	Cardinality of Set Partitions and Spivey's Generalized Recurrence for
	Bell Numbers, to theorems on equivalence relations. To count the
	number of partial equivalence relations, we observe that counting
	partial equivalence relations over a set A is equivalent to counting
	all equivalence relations over all subsets of the set A. From this
	observation and the results on equivalence relations, we show that the
	cardinality of partial equivalence relations over a finite set of
	cardinality n is equal to the n+1-th Bell number.
795

Lawrence Paulson's avatar
Lawrence Paulson committed
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
[Twelvefold_Way]
title = The Twelvefold Way
author = Lukas Bulwahn <mailto:lukas.bulwahn@gmail.com>
topic = Mathematics/Combinatorics
date = 2016-12-29
notify = lukas.bulwahn@gmail.com
abstract =
  This entry provides all cardinality theorems of the Twelvefold Way.
  The Twelvefold Way systematically classifies twelve related
  combinatorial problems concerning two finite sets, which include
  counting permutations, combinations, multisets, set partitions and
  number partitions. This development builds upon the existing formal
  developments with cardinality theorems for those structures. It
  provides twelve bijections from the various structures to different
  equivalence classes on finite functions, and hence, proves cardinality
  formulae for these equivalence classes on finite functions.

Lawrence Paulson's avatar
Lawrence Paulson committed
813
814
815
816
817
818
[Chord_Segments]
title = Intersecting Chords Theorem
author = Lukas Bulwahn <mailto:lukas.bulwahn@gmail.com>
notify = lukas.bulwahn@gmail.com
date = 2016-10-11
topic = Mathematics/Geometry
Lawrence Paulson's avatar
Lawrence Paulson committed
819
abstract =
820
821
822
823
824
825
826
827
828
	This entry provides a geometric proof of the intersecting chords
	theorem. The theorem states that when two chords intersect each other
	inside a circle, the products of their segments are equal.  After a
	short review of existing proofs in the literature, I decided to use a
	proof approach that employs reasoning about lengths of line segments,
	the orthogonality of two lines and the Pythagoras Law. Hence, one can
	understand the formalized proof easily with the knowledge of a few
	general geometric facts that are commonly taught in high-school.  This
	theorem is the 55th theorem of the Top 100 Theorems list.
Lawrence Paulson's avatar
Lawrence Paulson committed
829

830
831
832
833
834
[Category3]
title = Category Theory with Adjunctions and Limits
author = Eugene W. Stark <mailto:stark@cs.stonybrook.edu>
notify = stark@cs.stonybrook.edu
date = 2016-06-26
nipkow's avatar
nipkow committed
835
topic = Mathematics/Category theory
Lawrence Paulson's avatar
Lawrence Paulson committed
836
abstract =
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
	This 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.
870
871
872
873
874
extra-history =
	Change history:
	[2018-05-29]:
	Revised axioms for the category locale.  Introduced notation for composition and "in hom".
	(revision 8318366d4575)<br>
Eugene W. Stark's avatar
Eugene W. Stark committed
875
876
877
878
	[2020-02-15]:
	Move ConcreteCategory.thy from Bicategory to Category3 and use it systematically.
	Make other minor improvements throughout.
	(revision a51840d36867)<br>
879

nipkow's avatar
nipkow committed
880
881
882
[MonoidalCategory]
title = Monoidal Categories
author = Eugene W. Stark <mailto:stark@cs.stonybrook.edu>
nipkow's avatar
nipkow committed
883
topic = Mathematics/Category theory
nipkow's avatar
nipkow committed
884
885
date = 2017-05-04
notify = stark@cs.stonybrook.edu
886
abstract =
nipkow's avatar
nipkow committed
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
  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.
904
905
906
907
908
909
910
911
extra-history =
	Change history:
	[2017-05-18]:
	Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter.
	(revision 015543cdd069)<br>
	[2018-05-29]:
	Modifications required due to 'Category3' changes.  Introduced notation for "in hom".
	(revision 8318366d4575)<br>
Eugene W. Stark's avatar
Eugene W. Stark committed
912
913
914
	[2020-02-15]:
	Cosmetic improvements.
	(revision a51840d36867)<br>
nipkow's avatar
nipkow committed
915

916
917
918
919
920
921
[Card_Multisets]
title = Cardinality of Multisets
author = Lukas Bulwahn <mailto:lukas.bulwahn@gmail.com>
notify = lukas.bulwahn@gmail.com
date = 2016-06-26
topic = Mathematics/Combinatorics
Lawrence Paulson's avatar
Lawrence Paulson committed
922
abstract =
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
	<p>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.</p>  <p>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.</p>
938

939
940
941
942
943
[Posix-Lexing]
title = POSIX Lexing with Derivatives of Regular Expressions
author = Fahad Ausaf <http://kcl.academia.edu/FahadAusaf>, Roy Dyckhoff <https://rd.host.cs.st-andrews.ac.uk>, Christian Urban <http://www.inf.kcl.ac.uk/staff/urbanc/>
notify = christian.urban@kcl.ac.uk
date = 2016-05-24
nipkow's avatar
nipkow committed
944
topic = Computer science/Automata and formal languages
Lawrence Paulson's avatar
Lawrence Paulson committed
945
abstract =
946
947
948
949
950
951
952
953
954
955
956
	Brzozowski 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. In
	this entry 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). We also prove the correctness of an optimised
	version of the POSIX matching algorithm.
957

Lawrence Paulson's avatar
Lawrence Paulson committed
958
959
960
[LocalLexing]
title = Local Lexing
author = Steven Obua <mailto:steven@recursivemind.com>
nipkow's avatar
nipkow committed
961
topic = Computer science/Automata and formal languages
Lawrence Paulson's avatar
Lawrence Paulson committed
962
963
964
965
966
967
968
969
970
971
972
973
974
date = 2017-04-28
notify = steven@recursivemind.com
abstract =
  This formalisation accompanies the paper <a
  href="https://arxiv.org/abs/1702.03277">Local
  Lexing</a> which introduces a novel parsing concept of the same
  name. The paper also gives a high-level algorithm for local lexing as
  an extension of Earley's algorithm. This formalisation proves the
  algorithm to be correct with respect to its local lexing semantics. As
  a special case, this formalisation thus also contains a proof of the
  correctness of Earley's algorithm. The paper contains a short
  outline of how this formalisation is organised.

975
[MFMC_Countable]
Lawrence Paulson's avatar
Lawrence Paulson committed
976
title = A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Lars Hupel's avatar
Lars Hupel committed
977
author = Andreas Lochbihler <http://www.andreas-lochbihler.de>
978
date = 2016-05-09
nipkow's avatar
nipkow committed
979
topic = Mathematics/Graph theory
Lawrence Paulson's avatar
Lawrence Paulson committed
980
abstract =
Lars Hupel's avatar
Lars Hupel committed
981
982
983
984
985
986
987
988
989
990
991
992
	This article formalises a proof of the maximum-flow minimal-cut
	theorem for networks with countably many edges.  A network is a
	directed graph with non-negative real-valued edge labels and two
	dedicated vertices, the source and the sink.  A flow in a network
	assigns non-negative real numbers to the edges such that for all
	vertices except for the source and the sink, the sum of values on
	incoming edges equals the sum of values on outgoing edges.  A cut is a
	subset of the vertices which contains the source, but not the sink.
	Our theorem states that in every network, there is a flow and a cut
	such that the flow saturates all the edges going out of the cut and is
	zero on all the incoming edges.  The proof is based on the paper
	<emph>The Max-Flow Min-Cut theorem for countable networks</emph> by
Andreas Lochbihler's avatar
Andreas Lochbihler committed
993
	Aharoni et al.  Additionally, we prove a characterisation of the
Lars Hupel's avatar
Lars Hupel committed
994
995
996
	lifting operation for relations on discrete probability distributions,
	which leads to a concise proof of its distributivity over relation
	composition.
997
notify = mail@andreas-lochbihler.de
Andreas Lochbihler's avatar
Andreas Lochbihler committed
998
999
1000
extra-history =
	Change history:
	[2017-09-06]: