[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/
通比牛牛外挂下载 江苏11选5玩法秘籍 内蒙11选五开奖结果85 一码中大公开你敢买吗 手机炒股软件哪个好用 排列三有计划可寻吗 怎么买股票新手入门 上海天天选四今天开奖 七星彩开奖历史全部 好运彩下载 股票新手