报告题目：Can we make readable formal proofs ?

报告人：Jean-Jacques Lévy (Senior Researcher)

主持人：张敏

报告时间：12月12日（周二）9:30—10::30

报告地点：中北校区理科大楼B1002

报告摘要：

Formal proofs are usually very long. They are hardly checkable by humans, and the assistance of a computer is needed. Although it seems quasi impossible to read the details of the formal proof of a complex system, or an optimizing compiler, or an operating system or a many-cases program, one could envision possible to read the formal proofs of elegant but tricky algorithms with some help of automatic provers. In this talk, we take the examples of algorithms on graphs (depth-first-search, random-search, strongly connected components) and try to demonstrate that readability can be acheived modulo a bit of abstraction.

报告人简介：

Jean-Jacques Lévy graduated from the Ecole polytechnique in Paris, PhD at Univ. of Paris 7. He worked on optimal reductions in the lambda-calculus, on properties of term rewriting systems, and on concurrency theory. He has been appointed as a professor of Computer Science at the Ecole polytechnique in Palaiseau (1992-2008) and as the managing director of the new Microsoft Research-Inria Joint Centre in Paris (2006-2012). He is presently Senior Researcher emeritus at Inria in Univ. of Paris 7. His current research is on formal proofs of programs. He also participated to the debugging of the embedded code of the Ariane 5 (after its explosion in 1996) and directed the review of the embedded code of the Columbus module of the ISS (1998). He was a member of the research staff at DEC (1986-1988), and visiting professor at Iscas (2013-2014).