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 ------------------------------------------------------------------------------ HPCC Systems Open Source Big Data Platform from LexisNexis Risk Solutions Find What Matters Most in Your Big Data with HPCC Systems Open Source. Fast. Scalable. Simple. Ideal for Dirty Data. Leverages Graph Analysis for Fast Processing & Easy Data Exploration http://p.sf.net/sfu/hpccsystems _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
