coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] QED+20: Call for participation

From: Josef Urban <josef.urban AT gmail.com>
To: mizar-forum <mizar-forum AT mizar.uwb.edu.pl>, isabelle-users <isabelle-users AT cl.cam.ac.uk>, hol-info <hol-info AT lists.sourceforge.net>, coq-club <coq-club AT inria.fr>, math-wikis <math-wikis AT googlegroups.com>, Foundations of Mathematics <fom AT cs.nyu.edu>, projects-mkm-ig <projects-mkm-ig AT lists.jacobs-university.de>, om AT openmath.org, types AT lists.chalmers.se, theorem-provers <theorem-provers AT ai.mit.edu>, theory-logic AT cs.cmu.edu, users AT activemath.org, project-calculemus AT lists.jacobs-university.de
Subject: [Coq-Club] QED+20: Call for participation
Date: Thu, 12 Jun 2014 15:45:25 +0200

QED+20: Twenty Years of the QED Manifesto
July 18, 2014, Vienna, Austria
http://vsl2014.at/meetings/QED-index.html

CALL FOR PARTICIPATION

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.

SPEAKERS AND PROGRAMME:

http://vsl2014.at/meetings/QED-program.html

John Harrison: QED: a grand unified theory?

Georges Gonthier: How to prove the odd order from the four color theorem

Adam Grabowski: 25 years of the Mizar Mathematical Library

Gerwin Klein: The seL4 microkernel verification

Magnus Myreen and Ramana Kumar: Towards Formally Verified Theorem Provers

Claudio Sacerdoti Coen: TBA

Thomas C. Hales: TBA

Michael Beeson: Mixing proofs and computations

Marcos Cramer: The Naproche system: Proof-checking mathematical texts
in controlled natural language

Geoff Sutcliffe: QED and the TPTP World

Michael Kohlhase: MathHub.info: Active Mathematics

Cezary Kaliszyk: Hammering towards QED

Panel Discussion

ORGANIZERS:

John Harrison, Josef Urban, Freek Wiedijk

http://vsl2014.at/meetings/QED-index.html

[Coq-Club] QED+20: Call for participation, Josef Urban, 06/12/2014