Iowa Type Theory Commute
Iowa Type Theory Commute
Aaron Stump
Isabelle/HOL
16 minutes Posted Jan 28, 2022 at 5:00 am.
0:00
16:54
Download MP3
Show notes

The Isabelle theorem prover supports different logics, but its most developed seems to be Higher-Order Logic (HOL).  In this episode, I talk about the logic and approach of Isabelle/HOL, as far as I have understood them.