A SELECTED BIBLIOGRAPHY ON FORMALISED MATHEMATICS

1

Jeremy Avigad.
Notes on the formalization of the prime number theorem.
available at http://www.andrew.cmu.edu/user/avigad/Papers/pntnotes_a4.pdf.

2

Anthony Bailey.
Representing algebra in LEGO.
Master's Thesis, University of Edinburgh, 1993.

3

Anthony Bailey.
The machine-checked literate formalisation of algebra in type theory.
Phd Thesis, Manchester University, 1999.

4

Gertrud Bauer.
The 5 Colour Theorem in Isabelle/Isar.
In TPHOLs 2002, volume 1125, pages 141-156, Turku, Finland, 1996. Springer-Verlag.

5

Venanzio Capretta.
Abstraction and Computation.
Phd Thesis, University of Nijmegen, 2002.

6

Jan Cederquist.
A pointfree approach to constructive analysis in type theory.
Phd Thesis, Chalmers University of Technology and University of Goteborg, 1997.

7

Edmund M. Clarke and Xudong Zhao.
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.
In Conference on Automated Deduction, pages 758-763, 1994.

8

Nicolas G. de Bruijn.
A survey of the project AUTOMATH.
In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.

9

Bruno Dutertre.
Elements of mathematical analysis in PVS.
In Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs '96, volume 1125, pages 141-156, Turku, Finland, 1996. Springer-Verlag.

10

Jacques D. Fleuriot.
A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia.
Automated reasoning series: 2. Springer-Verlag, 2001.

11

Ruben A. Gamboa.
Mechanically Verifying Real-Valued Algorithms in ACL2.
Phd Thesis, University of Texas at Austin, 1999.

12

Herman Geuvers, Freek Wiedijk, and Jan Zwanenburg.
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.
In TYPES, pages 96-111, 2000.

13

Georges Gonthier.
A computer-checked proof of the four-colour theorem.
available at http://research.microsoft.com/ gonthier/4colproof.pdf.

14

Hanne Gottliebsen.
Transcendental Functions and Continuity Checking in PVS.
In TPHOLs 2000, volume 1869, pages 197-214, Portland, 2000. Springer-Verlag.

15

John Harrison.
Theorem Proving with the Real Numbers.
Springer-Verlag, 1998.

16

Gerard Huet and Amokrane Saïbi.
Constructive category theory.
In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998.

17

Joe Hurd.
Formal Verification of Probabilistic Algorithms.
Phd Thesis, University of Cambridge, 2002.

18

Paul B. Jackson.
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra.
Phd Thesis TR95-1509, Cornell University, 1995.

19

Micaela Mayero.
The Three Gap Theorem (Steinhauss Conjecture).
In Proceedings of TYPES'99, Lökeberg. Springer-Verlag LNCS, 1999.

20

William McCune.
Solution of the robbins problem.
Journal of Automated Reasoning, 19(3):263-276, 1997.

21

Mizar.
Journal of Formalized Mathematics.
http://mizar.org/JFM/.

22

Henrik Persson.
Type Theory and the Integrated Logic of Programs.
Phd Thesis, Göteborg University, 1999.

23

Art Quaife.
Automated development of fundamental mathematical theories.
Automated reasoning series: 2. Kluwer, 1992.

24

Natarajan Shankar.
Metamathematics, Machines, and Gödel's Proof.
Cambridge Tracts in Theoretical Computer Science: 38. Cambridge University Press, 1994.

25

Laurent Théry.
A Machine-Checked Implementation of Buchberger's Algorithm.
Journal of Automated Reasoning, 26:107-137, 2001.