{"id":6617,"date":"2020-07-31T17:36:51","date_gmt":"2020-07-31T09:36:51","guid":{"rendered":"https:\/\/www.zlaire.net\/events\/previous\/?p=6617"},"modified":"2020-07-31T18:07:05","modified_gmt":"2020-07-31T10:07:05","slug":"bruno-bentzen","status":"publish","type":"post","link":"https:\/\/www.zlaire.net\/events\/previous\/2020\/07\/bruno-bentzen\/","title":{"rendered":"Bruno Bentzen: Perspectives on the Foundations of Type Theory"},"content":{"rendered":"<p><strong>\u897f\u6eaa\u903b\u8f91\u8bba\u575b\u7b2c140\u671f<\/strong><\/p>\n<p><strong>Date:<\/strong> 7 August, 2020 (21:00-22:00)<\/p>\n<p><strong>Platform:<\/strong> Zheda Ding<br \/>\n<strong>Speaker:<\/strong> Dr. Bruno Bentzen (Carnegie Mellon University, USA)<\/p>\n<p><strong>Title:<\/strong> Perspectives on the foundations of type theory<br \/>\n<strong>Abstract:<\/strong> Type theory is a class of formal theories inspired by Russell&#8217;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\u2013Howard 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.<br \/>\n<strong>Short Bio:<\/strong> 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.<\/p>\n<p><strong>QR Code\uff1a<\/strong><\/p>\n<p><img decoding=\"async\" class=\"alignnone size-medium wp-image-6626 lazyload\" data-src=\"https:\/\/www.zlaire.net\/events\/previous\/wp-content\/uploads\/2020\/07\/webwxgetmsgimg-1-249x300.jpg\" alt=\"\" width=\"249\" height=\"300\" data-srcset=\"https:\/\/www.zlaire.net\/events\/previous\/wp-content\/uploads\/2020\/07\/webwxgetmsgimg-1-249x300.jpg 249w, https:\/\/www.zlaire.net\/events\/previous\/wp-content\/uploads\/2020\/07\/webwxgetmsgimg-1.jpg 645w\" data-sizes=\"(max-width: 249px) 100vw, 249px\" src=\"data:image\/svg+xml;base64,PHN2ZyB3aWR0aD0iMSIgaGVpZ2h0PSIxIiB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciPjwvc3ZnPg==\" style=\"--smush-placeholder-width: 249px; --smush-placeholder-aspect-ratio: 249\/300;\" \/><\/p>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>\u897f\u6eaa\u903b\u8f91\u8bba\u575b\u7b2c140\u671f 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&#8217;s conviction that every <span class=\"excerpt-dots\">&hellip;<\/span> <a class=\"more-link\" href=\"https:\/\/www.zlaire.net\/events\/previous\/2020\/07\/bruno-bentzen\/\"><span class=\"more-msg\">Continue reading &rarr;<\/span><\/a><\/p>\n","protected":false},"author":11,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"ngg_post_thumbnail":0,"footnotes":""},"categories":[1],"tags":[],"class_list":["post-6617","post","type-post","status-publish","format-standard","hentry","category-invited-talks"],"_links":{"self":[{"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/posts\/6617","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/comments?post=6617"}],"version-history":[{"count":5,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/posts\/6617\/revisions"}],"predecessor-version":[{"id":6627,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/posts\/6617\/revisions\/6627"}],"wp:attachment":[{"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/media?parent=6617"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/categories?post=6617"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.zlaire.net\/events\/previous\/wp-json\/wp\/v2\/tags?post=6617"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}