#7 Hacking Isabelle's Internals - Daniel Matichuk
Type Theory Forall
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.
Next Episodes
#6 All The Dumb Questions on Gradual Types - Zeina Migeed @ Type Theory Forall
📆 2021-03-29 06:00 / ⌛ 00:39:13
#5 The History of Coq'Art - Yves Bertot @ Type Theory Forall
📆 2021-02-27 05:00 / ⌛ 01:11:45
#4 Theorem Provers, Functional Programming and Companies - Eric Bond @ Type Theory Forall
📆 2021-02-15 05:00 / ⌛ 01:14:22
#3 ML for PL and Mental Health - Dan Zheng @ Type Theory Forall
📆 2021-02-01 05:00 / ⌛ 01:08:01
#2 Grad School Life - Rajan Walia and John Sarracino @ Type Theory Forall
📆 2021-01-10 05:00 / ⌛ 00:57:55