报告人：王盛颐（普林斯顿大学计算机系）
报告题目：形式化证明简介——以交互式定理证明助手 Coq 为例
报告时间：2021年3月18日 14:00
报告地点：文彬楼509
报告摘要：在当今，这个软件日益成为社会基础设施的时代，形式化证明作为一种用逻辑推理证明程序正确性的技术，也越发得到重视，具备广泛的应用前景。本报告以交互式定理证明助手 Coq 为例，介绍了形式化证明的基本概念，演示了如何使用 Coq 对如自然数、列表、树等归纳构造进行严格的形式化推理证明。
报告人简介：王盛颐，本科毕业于北京大学数学科学学院，博士毕业于新加坡国立大学，现任普林斯顿大学计算机系博士后研究员，长期从事基于交互式定理证明的程序验证研究。
邀请人：张华君 老师
