1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
2
3<html>
4
5<head>
6  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7  <title>The Isabelle Logo</title>
8</head>
9
10<body>
11
12<h1>The Isabelle Logo</h1>
13
14<h2>Versions</h2>
15
16The logo is available as bitmap file for the generic Isabelle system
17(<a href="#plain">plain</a>, <a href="#transparent">transparent</a>)
18and major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>,
19<a href="#HOLCF">HOLCF</a>).  There are also <a
20href="isabelle-small.xpm">small</a> and <a
21href="isabelle-tiny.xpm">tiny</a> Isabelle icons available.
22Furthermore, scalable (EPS) versions of the logo may be generated for
23any logic using the <tt>isabelle logo</tt> utility distributed with
24Isabelle.
25
26
27<h2>Interpretation</h2>
28
29<img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
30all, the logo tells about the name of the generic system, Isabelle, or
31of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
32some essentials of the overall Isabelle design philosophy: Composition
33of several small well understood building blocks, grouped together or
34arranged in layers. <p>
35
36The markings on the cubes illustrate this general principle by example
37of the core meta-logic (which is minimal higher-order logic on top of
38naively polymorphic simply typed lambda calculus). Thus red cubes
39symbolize the type system with function spaces (-&gt;) and type
40variables (alpha); violet ones represent the lambda term language with
41beta conversion etc.; yellow cubes constitute the actual logical
42parts, namely meta-implication or entailment (|-) and meta-level
43universal quantification.
44
45
46<h2>Acknowledgment</h2>
47
48The logo is contributed by <a
49href="http://www.informatik.tu-muenchen.de/~wenzel/">Franziska
50Wenzel</a>, Munich.  It has been designed on Apple Macintosh.
51
52
53<p><hr><p>
54
55<a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>
56
57<a name="transparent"><img src="isabelle_transparent.gif" alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
58black and white displays. <p>
59
60<a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo (ZF)]"></a> <p>
61
62<a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo (HOL)]"></a> <p>
63
64<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo (HOLCF)]"></a>
65
66</body>
67</html>
68