TWENTY YEARS OF THE QED MANIFESTO
"QED is the very tentative title of a project to build a computer system that effectively represents all important mathematical knowledge and techniques. The QED system will conform to the highest standards of mathematical rigor, including the use of strict formality in the internal representation of knowledge and the use of mechanical methods to check proofs of the correctness of all entries in the system..." (The QED Manifesto)
Overview
QED+20: Twenty Years of the QED Manifesto is a workshop commemorating the 20th anniversary of the QED Manifesto and the related 1994 and 1995 QED Workshops.
Aim
The workshop's goal is to show on real formal developments the state of the art in formalization of mathematics 20 years after QED. We want to discuss how we are (not yet) getting to the QED goals, what are the current issues and their proposed/prototyped/working solutions. We hope the workshop will be interactive and full of demonstrations and discussions.
Confirmed Speakers
Michael Beeson (San José State University)
Marcos Cramer (University of Luxembourg)
Georges Gonthier (Microsoft Research Cambridge)
Adam Grabowski (University of Bialystok)
John Harrison (Intel)
Thomas C. Hales (University of Pittsburgh)
Cezary Kaliszyk (University of Innsbruck)
Gerwin Klein (NICTA)
Michael Kohlhase (Jacobs University, Bremen)
Magnus Myreen and Ramana Kumar (University of Cambridge)
Claudio Sacerdoti Coen (University of Bologna)
Geoff Sutcliffe (University of Miami )
Publication
We plan to organize a special issue of the Journal of Formal Reasoning after this workshop on the QED+20 topics.