![Type Theory Forall artwork](https://is5-ssl.mzstatic.com/image/thumb/Podcasts124/v4/ed/de/43/edde43db-febe-b892-3a30-358ebe2e2c07/mza_16532267942080647912.png/100x100bb.jpg)
#7 Hacking Isabelle's Internals - Hacking Isabelle's Internals
Type Theory Forall
English - April 16, 2021 02:15 - 1 hour - 76 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #6 All The Dumb Questions on Gradual Types - Zeina Migeed
Next Episode: #8 Cedille - Chris Jenkins
In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some time hacking on its internals.
Me and Daniel also talk about Mizar, Isar, the seL4, and how it is formalized.
Torwards the end of the episode we also talk a little about his current work on the binary analysis of Aarch32 Arm Archtecture at Galois.