External Links

    Journal: J. Formalized Reasoning

    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