Stream: General

Topic: Differences between Simple Type Theory and Isabelle/HOL

view this post on Zulip Bob Rubbens (Sep 15 2026 at 19:38):

Hi all,

The seven virtues of simple type theory has really improved my understanding of why simple type theory is a good foundation for a theorem prover. Now I'm curious to learn more about the differences between the type theory that Isabelle supports, and the type theory presented in seven virtues. In particular, I'm wondering about the extensions that Isabelle has done to make simple type theory practically usable, such as polymorphism. Seven virtues also mentions undefinedness, indefinite description, and multi-sortedness, which as far as I can tell Isabelle all supports. Is there a nice description out there somewhere of Isabelle's STT++? Are these really extensions to STT in Isabelle, or is there somehow a translation of, e.g., undefinedness in the frontend to some kind of encoding in plain STT?

I also don't understand what exactly needs to go into the kernel, and what goes outside of it. Going by the explanation in seven virtues, I'd expect that a kernel contains:

  1. An implementation of an interpreter, for evaluating function application
  2. A type checker
  3. A proof system, e.g. to keep track of the proof steps using the axiom schemas as defined in section 6.
  4. Some notion of substitutibility, which is only explained in prose in seven virtues but probably also pretty important to get right, I reckon?

What I find confusing is that I've read on the internet that the kernel only needs part 1, an implementation of the interpreter. Is that the case? How are part 2 and 3 included without mistakes then?

(For completeness, my background is formal methods with an eye towards industry, which explains why finding good sources and understanding all this material remains challenging for me)

view this post on Zulip Kevin Kappelmann (Sep 15 2026 at 20:09):

Hi Bob, below paper by Kuncar and Popescu deals with the consistency of Isabelle/HOL's axioms.
https://link.springer.com/article/10.1007/s10817-018-9454-8

Function application is just beta reduction, which is one of the axioms of Isabelle.
The type checker is part of the kernel.
The proof system is part of the kernel.
Type and term instantiation are Isabelle axioms.

Last updated: Oct 05 2026 at 04:40 UTC