# The Isabelle Logo

## Versions

The logo is available as bitmap file for the generic Isabelle system
(plain, transparent)
and major object logics (ZF, HOL,
HOLCF). There are also small and tiny Isabelle icons available.
Furthermore, scalable (EPS) versions of the logo may be generated for
any logic using the `isatool logo` utility distributed with
Isabelle.
## Interpretation

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.
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 (->) 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.

## Acknowledgment

The logo is contributed by Franziska
Wenzel, Munich. It has been designed on Apple Macintosh.

Note: This may look bad on
black and white displays.