VSL 2014: VIENNA SUMMER OF LOGIC 2014
QED Home Page

 TWENTY YEARS OF THE QED MANIFESTO

QED-1994QED1995

 "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.

Organization

Program Committee