Jean-François Monin是法国Grenoble Alpes大学的教授，也是该校信息学系的系主任。他的研究方向是形式验证，主要关注如何用形式方法证明工业框架下软件的正确性。他致力于研究Coq。Coq是一个基于类型理论的形式证明系统，在分布式算法、安全和嵌入式软件领域有广泛应用。他也是“Understanding Formal Methods”一书的作者，该书介绍了该领域的多个最新技巧。
受包云岗研究员的邀请， Jean-François Monin教授于2016年12月14日来计算所交流并做了题为“Applications of Coq, a Proof Assistant based on Type Theory”的学术报告。该报告于上午10点30分在计算所四层报告厅举行。
在本次报告中，Jean-François Monin教授对Coq进行了介绍。报告介绍了Coq最突出的特性，解释了为什么这些特性能让Coq如此流行，尤其是在领域特定语言（DSL）中。一个多小时的演讲内容丰富，使得参加报告的老师和同学们受益匪浅。最后，在大家的掌声中结束了本次学术报告。
在会后的提问环节，参会的老师和同学们就编程语言的图灵完全性等话题与Jean-François Monin教授进行了深入讨论。感谢Jean-François Monin教授给我们带来这次精彩的报告。
 附件下载： |
合作交流