The Isabelle Logo


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.


[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.

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.


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

[Isabelle logo]

[Isabelle logo (transparent)] Note: This may look bad on black and white displays.

[Isabelle logo

[Isabelle logo

[Isabelle logo