TIME:
10-25-2022 16:30-18:30
SPEAKER:
Lawrence Paulson
Professor of Computational Logic
Computer Laboratory
University of Cambridge,UK
ABSTRACT:
The first talk is entitled “Type Theory and Logic”. It covers the history of type theory from Russell and Whitehead’s Principia Mathematica to modern dependent type theories, including how the idea of intuitionism led to Martin-Löf’s type theory and how Principia led to simple type theory, also known as higher-order logic.
The second talk is entitled “Formalised Mathematics: Obstacles and Achievements”. The first half will survey the history of the formalisation of mathematics by computer from 1958 until the present day. Then it describes in more detail some of the latest achievements done in Isabelle/HOL and Lean, with remarks on the research issues that still need to be overcome.
CHAIR:
Bruno Bentzen (Zhejiang University)