TypeSig Talks: Philip Wadler

Yesterday was another successful TypeSig Talk!

Our speaker was Prof. Philip Wadler, who needs no introduction. One of the principal designers of Haskell, Phil is a beloved lecturer here in Edinburgh, and was kind enough to give an introductory talk on formalising the lambda calculus in Lean 4. He covered basic proof techniques in Lean for those who had not seen them, then went on to give a brief representation of terms, and ended with a proof that 2+2=4.

Thanks to everyone who came, and special thanks to Phil in particular.