[11-20] Logipedia: towards a Wikipedia of formal proofs

文章来源:  |  发布时间:2019-11-18  |  【打印】 【关闭

Title: Logipedia: towards a Wikipedia of formal proofs
Speaker: Gilles Dowek (Inria and école normale supérieure de Paris-Saclay)
Time: 10:00 a.m. November 20th, 2019
Venue: Lecture room (334),  Building 5, SKLCS, Institute of Software, CAS
Abstract: Formal computerized proofs are now a central tool in computer science and in mathematics. But, each system – Coq, HOL Light, Isabelle/HOL, PVS... – implements its own language and its own theory, limiting the interoperability between systems and the sustainability of these proofs. Logipedia is an, in progress, encyclopedia of formal proofs, expressed in various theories. It is based on the idea to express these theories in a new logical framework allowing bound variables, explicit proof-terms, computation rules, and peaceful co-existence of constructive and non constructive proofs. 
Bio: Gilles Dowek is a senior researcher at Inria and professor at the école normale supérieure de Paris-Saclay. He is interested in the formalization of mathematics, in proof processing systems, in the physics of computation, in the safety of aerospace systems, and in the epistemology and ethics of computer science. He is a member of the Scientific board of the  French computer science society and of the CERNA ethics committee. He has contributed to the computer science curricula in French high schools. In the past, he has been Deputy Scientific Director of Inria in charge of the domain Algorithmic, Programming, Software and Architectures. His book Les Métamorphoses du calcul (the metamorphoses of calculation) was awarded le Grand Prix de philosophie 2007 de l’Académie fran?aise. http://www.lsv.fr/~dowek/
友情链接:007彩票平台  六福彩票网站  亚冠游戏平台  uc彩票官方网址  久草资源站  北京赛车后三基本走势图  106平台彩票技巧  099彩票经验技巧  手机注册送金网站  送彩金的网站大白菜