External Links

    Journal: J. Formalized Reasoning

    Volume 3, Issue 2

    1 -- 93Adam J. Chlipala. An Introduction to Programming and Proving with Dependent Types in Coq
    95 -- 152Georges Gonthier, Assia Mahboubi. An introduction to small scale reflection in Coq
    153 -- 245Adam Grabowski, Artur Kornilowicz, Adam Naumowicz. Mizar in a Nutshell

    Volume 3, Issue 1

    1 -- 27Geoff Sutcliffe, Christoph Benzmüller. Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
    29 -- 48Bruno Barras. Sets in Coq, Coq in Sets
    49 -- 77Marco B. Caminati. Basic first-order model theory in Mizar
    79 -- 126José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
    runs on