<html>
<!-- $Id$ -->
<head>
<title>The Isabelle Logo</title>
</head>
<body>
<h1>The Isabelle Logo</h1>
<h2>Versions</h2>
The logo is available 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>).
<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 naively polymorphic simply typed
lambda calculus with minimal higher-order logic). Thus red cubes
symbolize the type system with function spaces (->) 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 Franziska Wenzel, Munich. Thanks
Franziska! <p>
<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> <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> <p>
</body>
</html>