THE FORMALIZATION / ISABELLE · HOL

A map of the
formalization.

Every exported fact, constant, type and locale. Explore the declarations behind Voblint’s soundness argument.

Loading Isabelle declarations…

Find a declaration

Session Kind

Only facts cited in the thesis

How to read this map

Sectors group declarations by Isabelle session; smaller wedges group theories. Each mark represents one exported entity, including automatically generated facts. Session colors follow the dependency layers of the site’s strata figure; each theory forms a streak. Ordinary declarations appear progressively as you zoom. Radial layers follow statement-reference distances from the main results; disconnected declarations occupy the outer band. These distances are not proof depth. Main results, thesis citations and filter matches remain visible at every scale. At close range, highlighted declarations and treemap cells become readable cards. Circles are facts, squares constants, triangles types and outlined diamonds locales. Shape becomes clearer as you zoom.

Select a declaration to see the project entities mentioned in its statement or specification. These lines do not track lemmas used inside proofs. Library entities outside the project are counted but not drawn.

Red stars mark selected source-level soundness results; gold diamonds mark facts cited in the thesis. A fact may be a theorem, lemma, definition equation, or generated rule; the export does not distinguish them.

Visual design inspired by the CFSG proof map.

Isabelle declarations

Color = dependency layer Fact Constant Type Locale Thesis citation★ Main result

Scroll to pan · pinch to zoom · click for documentation

Loading the corpus…