lib/logo/index.html
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 7807 6a102f74ad0a
child 15585 513aa9a3a26d
permissions -rw-r--r--
tuned;


<html>

<!-- $Id$ -->

<head>
<title>The Isabelle Logo</title>
</head>

<body>

<h1>The Isabelle Logo</h1>

<h2>Versions</h2>

The logo is available as bitmap file for the generic Isabelle system
(<a href="#plain">plain</a>, <a href="#transparent">transparent</a>)
and major object logics (<a href="#ZF">ZF</a>, <a href="#HOL">HOL</a>,
<a href="#HOLCF">HOLCF</a>).  There are also <a
href="isabelle-small.xpm">small</a> and <a
href="isabelle-tiny.xpm">tiny</a> Isabelle icons available.
Furthermore, scalable (EPS) versions of the logo may be generated for
any logic using the <tt>isatool logo</tt> utility distributed with
Isabelle.


<h2>Interpretation</h2>

<img src="isabelle.gif" align=right alt="[Isabelle logo]"> First of
all, the logo tells about the name of the generic system, Isabelle, or
of its concrete instantiations, e.g. Isabelle/HOL.  It also expresses
some essentials of the overall Isabelle design philosophy: Composition
of several small well understood building blocks, grouped together or
arranged in layers. <p>

The markings on the cubes illustrate this general principle by example
of the core meta-logic (which is minimal higher-order logic on top of
naively polymorphic simply typed lambda calculus). Thus red cubes
symbolize the type system with function spaces (-&gt;) and type
variables (alpha); violet ones represent the lambda term language with
beta conversion etc.; yellow cubes constitute the actual logical
parts, namely meta-implication or entailment (|-) and meta-level
universal quantification.


<h2>Acknowledgment</h2>

The logo is contributed by <a
href="http://www.informatik.tu-muenchen.de/~wenzel/">Franziska
Wenzel</a>, Munich.  It has been designed on Apple Macintosh.


<p><hr><p>

<a name="plain"><img src="isabelle.gif" alt="[Isabelle logo]"></a> <p>

<a name="transparent"><img src="isabelle_transparent.gif"
alt="[Isabelle logo (transparent)]"></a> Note: This may look bad on
black and white displays.  <p>

<a name="ZF"><img src="isabelle_zf.gif" alt="[Isabelle logo
(ZF)]"></a> <p>

<a name="HOL"><img src="isabelle_hol.gif" alt="[Isabelle logo
(HOL)]"></a> <p>

<a name="HOLCF"><img src="isabelle_holcf.gif" alt="[Isabelle logo
(HOLCF)]"></a>

</body>
</html>