12月10日,电子科技大学人文社科高等研究院成功举办第二十期“人文×科技”思想者论坛。本次论坛以“现代类型论的发展与应用”为主题,特邀伦敦大学皇家霍洛威学院计算机系教授、现代类型论及其应用领域的学术带头人罗朝晖教授担任主讲嘉宾,万小龙教授担任主持人。
万教授对罗教授的到来表示热烈欢迎与诚挚感谢,并简要介绍了罗教授的主要研究领域与前沿成果。罗教授毕其一生精力研究现代类型论及其应用,取得了卓越的研究成果,原创作品包括研究统一类型论的《计算与推理》、研究自然语言语义学的《基于现代类型论的形式语义学》以及中文专著《现代类型论的发展与应用》。

讲讲座中,罗教授首先梳理了现代类型论的发展脉络与理论体系构成。他指出,类型论的演进历经从罗素悖论的提出,到分支类型论的建构,再到简单类型论的完善,最终发展为现代类型论的完整体系。现代类型论涵盖依赖类型、归纳类型等复杂类型结构,可划分为直谓性与非直谓性两大类别。

随后,罗教授将视角转向现代类型论的元理论及其应用,特别强调了类型论在自然语言语义学中的应用。他还提到了现代类型论在数学技术形式化推理和计算机交互性定理证明等方面的应用,并对现代类型论的未来发展进行了展望。此外,罗教授还分享了他对现代类型论的一些理解和看法,以及如何将类型论应用于实际研究中的建议。

在提问互动环节,现场师生现场师生围绕“白马非马”等问题与罗教授展开深入交流。罗教授结合自身研究经验,逐一回应了师生疑问,强调对于抽象对象应灵活使用,而不是单纯依赖指称,以及如何将证明转化为标准形式进行计算机逻辑判断。

最后,万教授对本次讲座进行总结,再次对罗教授表示诚挚感谢,并鼓励有志于研究的学生积极参与,贡献专业智慧。本次讲座为现场师生带来了丰富的学术滋养,既系统梳理了现代类型论的核心知识,又提供了宝贵的研究指导,充分彰显了学术分享的价值,对助力相关领域师生的学术成长、推动学科交叉融合发展具有重要意义。
