逸仙逻辑讲坛第二十八期预告｜Bruno Bentzen ：构造语义中的 Church-Curry 类型

第二十八期  逸仙逻辑讲坛

题目：构造语义中的 Church-Curry 类型

主讲人：Bruno Bentzen  助理教授

           浙江大学太阳集团城娱8722

主持人：王   玮  教授

           太阳集团城娱8722逻辑与认知研究所

时   间：4月11日（周五）下午15:00

地   点：太阳集团tcy8722锡昌堂322室

主办方：太阳集团tcy8722逻辑与认知研究所

主讲人简介 

       Bruno Bentzen 是浙江大学太阳集团城娱8722助理教授，他在太阳集团tcy8722逻辑与认知研究所获得博士学位。他的研究领域是逻辑和数学哲学，特别关注数学建构主义和构造类型理论的传统。他在 Review of Symbolic Logic, Notre Dame Journal of Formal Logic, Philosophia Mathematica, History and Philosophy of Logic 和 Erkenntnis 等期刊上发表过多篇文章。在加入浙江大学之前，他曾在卡内基梅隆大学和捷克科学院担任博士后。

内容简介 

       类型论中有两种主要的类型化风格。在 Church 风格的类型化下，表达式的类型是其固有属性之一，就像指纹是人身份的内置特征一样。在 Curry 的风格下，类型被分配给无类型语言的表达式，就像护照在出生后识别一个人一样。我在这个演讲中的目的是阐明 Brouwer、Heyting、Kolmogorov 等人开发的构造语义学背景下的这种类型化区别。我将假设 Martin-Löf 为他的构造类型理论开发的意义解释。更准确地说，我想在意义解释中对比 Church 和 Curry 两种风格的哲学和技术优势。我特别认为，Martin-Löf 后期作品中采用 Church 风格的类型化求值 (typed evaluation) 导致了循环解释。