Type Theory Forall

Type Theory much beyond inference rules

Episode image

#24 The History of Isabelle

Lawrence Paulson

Apr 11th 2024   |  98 min

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!



join our discord