报告人: 王迪 （北京大学计算机学院）

题目：直觉主义逻辑与程序设计语言

时间：2023/03/28 15:10-18:00

地点：二教 501

摘要：

直觉主义逻辑（也称为构造性逻辑）相比于经典逻辑，注重证实性而非真理性，具体可以体现在对否定以及排中律的处理上。直觉主义逻辑下的证明是构造性的，一个命题的证明可视为构造了一个证据。在柯里-霍华德同构意义下，人们通过“命题即类型”、“证明即程序”建立了直觉主义逻辑与计算间的关系，即“证据M给出了命题A的证明”可解释为“程序M具有类型A”。在同构意义下，逻辑具备了可计算性。在本报告中，我们将讨论直觉主义逻辑视角下的编程语言设计，不同的逻辑系统将对应不同的类型系统，对证明的不同规约方式将对应不同的的计算模型。逻辑与计算的协同设计为设计编程语言提供了系统的理论指引，保证了语言设计的一致性。具体而言，报告将讨论直觉主义命题逻辑-函数式编程、直觉主义线性逻辑-消息传递并发编程、直觉主义模态逻辑-阶段化编程三个对应实例，并探讨新兴计算模型（如概率编程）下适用的逻辑系统。

个人简介：

王迪是北京大学计算机学院的助理教授，是程序设计语言研究室的成员。王迪对编程语言的多个研究话题都很有兴趣，尤其是形式化验证、程序分析以及概率编程。他希望构建适用于编写安全、高效的软件的通用、易用的编程抽象和范式，以及能够自动分析、优化、合成程序的编程语言工具链。他目前的研究项目主要涉及资源安全的系统编程、可编程贝叶斯推断、量化程序分析以及面向证明的编程语言。在加入北京大学前，王迪在卡内基梅隆大学获得计算机科学博士学位，导师为Jan Hoffmann教授。