【学术报告】3月18日普林斯顿博士后研究员王盛颐学术报告
   发布时间: 2021-03-09    访问次数: 455

报告人:王盛颐(普林斯顿大学计算机系)

报告题目:形式化证明简介——以交互式定理证明助手 Coq 为例

报告时间:2021318 14:00

报告地点:文彬楼509

报告摘要:在当今,这个软件日益成为社会基础设施的时代,形式化证明作为一种用逻辑推理证明程序正确性的技术,也越发得到重视,具备广泛的应用前景。本报告以交互式定理证明助手 Coq 为例,介绍了形式化证明的基本概念,演示了如何使用 Coq 对如自然数、列表、树等归纳构造进行严格的形式化推理证明。

 

报告人简介:王盛颐,本科毕业于北京大学数学科学学院,博士毕业于新加坡国立大学,现任普林斯顿大学计算机系博士后研究员,长期从事基于交互式定理证明的程序验证研究。

 

邀请人:张华君  老师


计算机与人工智能学院
阿里云大数据学院

School of Computer Science and Artificial
Intelligence & Aliyun School of Big Data

联系我们
地址:江苏省常州市武进区滆湖中路21号(213164)
邮箱:bigdata@cczu.edu.cn
电话:0519-88519909
管理入口

扫描二维码关注

Copyright © 2019-2020 常州大学计算机与人工智能学院 阿里云大数据学院 All rights reserved.