Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto

QED 20th anniversary

• Preface: Twenty Years of the QED Manifesto

  John Harrison, Josef Urban, Freek Wiedijk

  1 - 2

  • PDF

• Proof Auditing Formalised Mathematics

  Mark Miles Adams

  3 - 32

  • PDF

• Now f is continuous (exercise!)

  Robin Denis Arthan

  33 -52

  • PDF

• Formalizing Scientifically Applicable Mathematics in a Definitional Framework

  Arnon Avron, Liron Cohen

  53-70

  • PDF

• Mixing Computations and Proofs

  Michael Beeson

  71-99

  • PDF

• Hammering towards QED

  Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban

  101-148

  • PDF

• Theorema 2.0: Computer-Assisted Natural-Style Mathematics

  Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger

  149-185

  • PDF

• Conversion of HOL Light proofs into Metamath

  Mario M Carneiro

  187-200

  • PDF

• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge

  Michael Kohlhase, Florian Rabe

  201-234

  • PDF

• Mathematical Text Processing in EA-style: a Sequent Aspect

  Alexander Lyaletski

  235-264

  • PDF