西溪逻辑论坛第140期

Date: 7 August, 2020 (21:00-22:00)

Platform: Zheda Ding
Speaker: Dr. Bruno Bentzen (Carnegie Mellon University, USA)

Title: Perspectives on the foundations of type theory
Abstract: Type theory is a class of formal theories inspired by Russell’s conviction that every term must have a type and every operation must be restricted to terms of a certain type. Since the discovery of the celebrated Curry–Howard correspondence between logic and type theory and the development of homotopical interpretations of equality, type theory has been gaining more acceptance as a foundational framework for mathematics. But for what reason should one prefer type theory over set theory and logic? In this lecture, I discuss some fundamental questions that must be answered before type theory can be considered as a serious alternative foundation.
Short Bio: Bruno Bentzen is a Postdoctoral Fellow in the Department of Philosophy at Carnegie Mellon University. He received his PhD in Logic from the Institute of Logic and Cognition in the Department of Philosophy at Sun Yat-sen University in 2019. His work focuses on the foundations of mathematical constructivism, varying from intuitionism and type theory to formal proof verification.

QR Code：