Jouannaud教授作报告

11月19日，法国国立信息与自动化研究院(INRIA)Jean-Pierre Jouannaud教授应中欧信息、自动化与应用数学联合实验室(LIAMA) 欧方主任、先进院特聘研究员Vania Joloboff教授的邀请在中科院深圳先进技术研究院进行学术交流，并作了题为Coq, a Language for Programming Correct Proofs的学术报告。

Jouannaud教授主要介绍了Coq编程语言及其在严格的定理证明中的应用。Jouannaud教授描述了类型理论(TypeTheory)如何通过Curry-Howard对应建立证明协助(Proof Assistants)，以及其在高阶逻辑(HOL)的延伸。Jouannaud教授列举了近十多年在数学和计算机科学中使用定理证明工具取得的重大成就，其中有大部分归功于Coq、HOL-Isabelle及HOL-Light的帮助。

本次讲座现场气氛热烈，研究人员和同学们在讲座后积极地和Jean-Pierre Jouannaud教授进行了广泛深入的交流和探讨。

Jean-Pierre Jouannaud教授1969年毕业于巴黎综合理工大学，1978年获得巴黎第六大学博士学位，之后担任法国南希大学、巴黎第十一大学和巴黎综合理工大学的教授，以及包括美国斯坦福研究所和斯坦福大学、西班牙巴萨罗那大学和日本庆应大学在内的多所大学的客座教授。Jean-Pierre Jouannaud教授现担任法国国立信息与自动化研究院(INRIA)研究主任、清华大学软件学院软件理论讲席教授。