法国国家信息与自动化研究院（INRIA Sophia-Antipolis） Yves Bertot
报告题目：Using the Coq system for the formal verification of mathematics
报告人： Yves Bertot 教授，
报告摘要：In mathematics, we can find three important ingredients:
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
著有Coq in a Hurry、Interactive Theorem Proving and Program Development:
Coq'Art: The Calculus of Inductive Constructions等书,