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.