![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)
#24 The History of Isabelle - Lawrence Paulson
Type Theory Forall
English - October 06, 2022 22:05 - 1 hour - 87.8 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich
Next Episode: #25 Formally Verifying the Tezos Codebase - Formal Land
In this episode we interview Lawrence Paulson, one of the creating fathers of
Isabelle.
We talk about the development process, how it drew inspirations and
ideas from LCF and Boyer Moore. What tools were used, it’s strenghts and
weaknesses, and all about the historical context at the time! We also briefly
talk about his formalization of the Gödel's Incompletenes theorems in Isabelle
Paulson have quite an extensive CV, he is a professor at Cambridge, have
published more than 100 papers, is an ACM fellow since 2008, is a member of
the royal society since 2017, among many other things!
Links