|
1 |
|
2 <html> |
|
3 |
|
4 <!-- $Id$ --> |
|
5 |
|
6 <head> |
|
7 <title>The Isabelle Logo</title> |
|
8 </head> |
|
9 |
|
10 <body> |
|
11 |
|
12 <h1>The Isabelle Logo</h1> |
|
13 |
|
14 <h2>Versions</h2> |
|
15 |
|
16 The logo is available for the generic Isabelle system (<a |
|
17 href="#plain">plain</a>, <a href="#transparent">transparent</a>) and |
|
18 major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>, <a |
|
19 href="#HOLCF">HOLCF</a>). |
|
20 |
|
21 |
|
22 <h2>Interpretation</h2> |
|
23 |
|
24 <img src="isabelle.gif" align=right alt="Isabelle logo"> First of all |
|
25 the logo tells about the name of the generic system, Isabelle, or of |
|
26 its concrete instantiations, e.g. Isabelle/HOL. It also expresses |
|
27 some essentials of the overall Isabelle design philosophy: Composition |
|
28 of several small well understood building blocks, grouped together or |
|
29 arranged in layers. <p> |
|
30 |
|
31 The markings on the cubes illustrate this general principle by example |
|
32 of the core meta-logic (which is naively polymorphic simply typed |
|
33 lambda calculus with minimal higher-order logic). Thus red cubes |
|
34 symbolize the type system with function spaces (->) and type variables |
|
35 (alpha); violet ones represent the lambda term language with beta |
|
36 conversion etc.; yellow cubes constitute the actual logical parts, |
|
37 namely meta-implication or entailment (|-) and meta-level universal |
|
38 quantification. |
|
39 |
|
40 |
|
41 <h2>Acknowledgment</h2> |
|
42 |
|
43 The logo is contributed by Franziska Wenzel, Munich. Thanks |
|
44 Franziska! <p> |
|
45 |
|
46 |
|
47 <p><hr><p> |
|
48 |
|
49 <a name="plain"><img src="isabelle.gif" alt="Isabelle logo"></a> <p> |
|
50 |
|
51 <a name="transparent"><img src="isabelle_transparent.gif" |
|
52 alt="Isabelle logo (transparent)"></a> <p> |
|
53 |
|
54 <a name="ZF"><img src="isabelle_zf.gif" alt="Isabelle logo (ZF)"></a> |
|
55 <p> |
|
56 |
|
57 <a name="HOL"><img src="isabelle_hol.gif" alt="Isabelle logo |
|
58 (HOL)"></a> <p> |
|
59 |
|
60 <a name="HOLCF"><img src="isabelle_holcf.gif" alt="Isabelle logo |
|
61 (HOLCF)"></a> <p> |
|
62 |
|
63 </body> |
|
64 </html> |