法国国家信息与自动化研究院（INRIA Sophia-Antipolis） Yves Bertot  
教授学术报告

报告题目：Using the Coq system for the formal verification of mathematics  
and
software

报告人： Yves Bertot 教授，
              INRIA Sophia-Antipolis

报告时间：2011年8月12日上午10：00-11：00
报告地点：计算机学院三楼会议室（一教南317）
报告摘要：In mathematics, we can find three important ingredients:  
structures and
data, algorithms, and proofs. Examples of structures and data are, on
the one hand algebraic structures like rings, fields, or vector spaces
and on the other hand natural numbers. Examples of algorithms are for
instance the algorithm to compute the greatest common divisor. Examples
of proofs are for instance, the proof that there is no rational number
whose square is 2. Based on these ingredients, mathematics exist only
because there are very precise rules that govern the way one can define
a new structure, the way one can define an algorithm, or the way one can
chain reasoning steps to make a proof. It has been accepted for a
century, that mathematics should be so precise that it could be verified
by a machine.

The Coq system has been designed with the aim of providing a powerful
framework to perform exactly this task: verify that mathematical
definitions and proofs do respect the precise rules that should govern
mathematics. The system contains definitions of basic mathematical
objects, it provides means to add new definitions and to describe
algorithms working on these mathematical objects. It also makes it
possible to write proofs and to show that these proofs are correct.

The situation of mathematics is close to the situation in computer
science, with respect to software development. Like mathematicians,
software developers have to define structures (data-structures), they
have to define algorithms (programs), and they have to reason about
their programs (especially when hunting down the bugs). Documenting
software for a software developer is similar to asserting properties
about structures and algorithms for a mathematician.

Using Coq, we can also describe software and show that this software
performs the intended task, that it has good propeties.

In this talk, I will present briefly the fundamental charateristics of
the Coq system and show how it can be applied in some areas of
mathematics (for instance, polynomial and linear algebra, arithmetics,
and group theory) and in some areas of computer science (for instance,
sorting, programming language design, compilation).

报告人简介：Yves Bertot是法国国家信息与自动化研究院(INRIA) Sophia  
Antipolis研究中心的高级研究员。他的主要研究兴趣是用定理证明工具来形式化描述算法和数学理论。他对高阶定理证明辅助工具Coq有相当深入的了解,  
著有Coq in a Hurry、Interactive Theorem Proving and Program Development:  
Coq'Art: The Calculus of Inductive Constructions等书,  
这些书是每个深入了解Coq的人必读的书目。目前Yves  
Bertot正带领开展Marelle项目,  
该项目的目标是研究和使用在计算机上检验保证软件正确性的数学证明的相关技术，开发一些方法和工具以便从对数据、算法及其性质的精确描述和这些性质的证明产生正确的程序。

欢迎广大师生参加交流！