[FOM] JFR Special Issue on QED+20 Published

[Josef Urban]

---------- Forwarded message ----------
From: Prof. Andrea Asperti <asperti at cs.unibo.it>
Date: Fri, Jan 29, 2016 at 9:10 AM
Subject: [JFR] New Issue Published
To: "Dr. Josef Urban" <josef.urban at gmail.com>




Dear readers:

the Journal of Formalized Reasoning has just published a special issue
devoted to the 20th anniversary of the QED manifesto. We invite you to
review the Table of Contents below and then visit our web site at
http://www.jfr.unibo.it to download articles and items of interest.

Thanks for the continuing interest in our work,
Andrea Asperti
University of Bologna
asperti at cs.unibo.it

Journal of Formalized Reasoning
Vol 9, No 1 (2016): Special Issue: Twenty Years of the QED Manifesto.
Table of Contents
http://jfr.unibo.it/issue/view/554

QED 20th anniversary
--------

Preface: Twenty Years of the QED Manifesto (1 - 2)
        John Harrison,  Josef Urban,    Freek Wiedijk
Proof Auditing Formalised Mathematics (3 - 32)
        Mark Miles Adams
Now f is continuous (exercise!) (33 -52)
        Robin Denis Arthan
Formalizing Scientifically Applicable Mathematics in a Definitional
Framework (53-70)
        Arnon Avron,    Liron Cohen
Mixing Computations and Proofs (71-99)
        Michael Beeson
Hammering towards QED (101-148)
        Jasmin C. Blanchette,   Cezary Kaliszyk,        Lawrence C.
Paulson,    Josef Urban
Theorema 2.0: Computer-Assisted Natural-Style Mathematics (149-185)
        Bruno Buchberger,       Tudor Jebelean, Temur Kutsia,   Alexander
Maletzky,       Wolfgang Windsteiger
Conversion of HOL Light proofs into Metamath (187-200)
        Mario M Carneiro
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
(201-234)
        Michael Kohlhase,       Florian Rabe
Mathematical Text Processing in EA-style: a Sequent Aspect (235-264)
        Alexander Lyaletski

________________________________________________________________________
Journal of Formalized Reasoning
http://jfr.cib.unibo.it