Bibliography

1

RELAX NG Specification, December 2001.
Available from http://www.relaxng.org/spec-20011203.html.

2

John Abbott, Angel Díaz, and Robert S. Sutor.
A report on OpenMath. A protocol for the exchange of mathematical information.
SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation), 30(1):21-24, 1996.

3

David Albrecht and John N. Crossley.
Program extraction, simplified proof-terms and realizability.
Technical Report 271, Department of Computer Science, Monash University, 1996.

4

Ahmed Amerkad, Yves Bertot, Loïc Pottier, and Laurence Rideau.
Mathematics and proof presentation in Pcoq.
Technical report, Institut National de Recherche en Informatique et en Automatique, November 2001.

5

David Aspinall.
Proof General: A generic tool for proof development.
In Tools and Algorithms for the Construction and Analysis, pages 38-42. Laboratory for Foundations of Computer Science, Springer, 2000.
LNCS 1785.

6

David Aspinall.
Protocols for Interactive e-Proof.
In 13th International Conference on Theorem Proving in Higher Order Logics. Laboratory for Foundations of Computer Science, May 2000.
Draft extended abstract, presented as a work-in-progress, available from http://homepages.inf.ed.ac.uk/da/papers/drafts/#eproof.

7

David Aspinall.
Proof General Kit white paper, July 2003.
Laboratory for Foundations of Computer Science, http://homepages.inf.ed.ac.uk/da/papers/drafts/#white.

8

Ron Ausbrooks, Stephen Buswell, Stéphane Dalmas, Stan Devitt, Angel Diaz, Roger Hunter, Bruce Smith, Neil Soiffer, Robert Sutor, and Stephen Watt.
Mathematical Markup Language (MathML) Version 2.0.
Technical report, World Wide Web Consortium, March 2000.
Edited by Nico Poppelier, Robert Miner, Patrick Ion and David Carlisle. Available from http://www.w3.org/TR/MathML2/.

9

Ron Avitzur.
Direct manipulation in a mathematics user interface, pages 43-60.
In Kajler [26], January 1999.

10

B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner.
The Coq Proof Assistant Reference Manual - Version 7.2.
Technical Report 0255, Institut National de Recherche en Informatique et en Automatique, February 2002.

11

Joseph L. Bates and Robert L. Constable.
Proofs as Programs.
Technical Report 82-530, Department of Computer Science, Cornell University, Ithaca, New York, USA, February 1983.

12

Janet Bertot and Yves Bertot.
CtCoq: A system presentation.
In Martin Wirsing and Maurice Nivat, editors, Algebraic Methodology and Software Technology, pages 600-603, Munich, July 1996. Springer.
LNCS.

13

Yves Bertot.
The CtCoq System: Design and Architecture.
Technical Report 3540, Institut National de Recherche en Informatique et en Automatique, October 1998.

14

Yves Bertot, Gilles Kahn, and Laurent Théry.
Proof by Pointing.
In Theoretical Aspects of Computer Software, volume 789, pages 141-160. Springer Verlag, April 1994.

15

P. Callaghan and Z. Luo.
An implementation of LF with coercive subtyping & universes.
Journal of Automated Reasoning, 27(1):3-27, July 2000.
Special Issue on Logical Frameworks and Metalanguages.

16

Anthony Cant and Mark Ozols.
XIsabelle: A Graphical User Interface to the Isabelle Theorem Prover (draft).
Technical report.
Available from ftp://ftp.cl.cam.ac.uk/ml/.

17

Robert L. Constable.
The structure of Nuprl's type theory, pages 123-156.
In Schwichtenberg [52], August 1997.

18

John N. Crossley and Iman Poernomo.
Fred: An Approach to Generating Real, Correct, Reusable Programs from Proofs.
Journal for Universal Computer Science (Online Edition), 7(1):71-88, 2001.

19

N.G. de Bruijn.
AUTOMATH, a Language for Mathematics.
In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pages 159-200. Springer, Berlin, Heidelberg, 1983.

20

David Evans and David Larochelle.
Splint Manual.
Secure Programming Group, University of Virginia Department of Computer Science, June 2003.
http://lclint.cs.virginia.edu/manual/.

21

Bob Glickstein.
Writing GNU Emacs Extensions.
O'Reilly and Associates, April 1997.

22

M. J. C. Gordon and T. F. Melham, editors.
Introduction to HOL: A theorem proving environment for higher order logic.
Cambridge University Press, 1993.

23

Elliotte Rusty Harold and W. Scott Means.
XML in a Nutshell.
In a Nushell series. O'Reilly and Associates, second edition, June 2002.

24

C. Michael Holloway.
Why engineers should consider formal methods.
In Proceedings of the 16th AIAA/IEEE Digital Avionics Systems Conference, page 7. NASA Langley Research Center, October 1997.

25

Michael R.A. Huth and Mark D. Ryan.
Logic in Computer Science - Modelling and reasoning about systems.
Cambridge University Press, 2000.

26

N. Kajler, editor.
Computer-Human Interaction in Symbolic Computation.
Springer, January 1999.

27

Matt Kaufmann and J. Moore.
An industrial strength theorem prover for a logic based on Common Lisp.
IEEE Transactions on Software Engineering, 23(4):203-213, April 1997.

28

John C. Knight, Colleen L. DeJong, Matthew S. Gribble, and Luís G. Nakano.
Why Are Formal Methods Not Used More Widely?
In Fourth NASA Formal Methods Workshop. University of Virginia, Department of Computer Science, September 1997.

29

Edmund Yehezkel Landau.
Grundlagen der Analysis.
Erstveröff, Leipzig, first edition, 1930.

30

David Larochelle and David Evans.
Statically detecting likely buffer overflow vulnerabilities.
In 10th USENIX Security Symposium, pages 177-190. University of Virginia, Department of Computer Science, USENIX Association, August 2001.

31

Nancy Leveson.
An investigation of the Therac-25 accidents.
Technical Report 92-11-05, University of Washington, 1992.

32

M. Lowry, A. Philpot, T. Pressburger, and I. Underwood.
Amphion: Automatic Programming for Scientific Subroutine Libraries, volume 869 of LNCS, pages 326-335.
Springer-Verlag, Charlotte, North Carolina, October 1994.

33

Zhaohui Luo and Randy Pollack.
LEGO Proof Development System: User's Manual.
Technical Report ECS-LFCS-92-211, School of Informatics, University of Edinburgh, 1992.

34

C. Lüth, H. Tej, and B. Krieg-Brückner Kolyang.
TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving.
In European Joint Conference on Theory and Practice of Software ETAPS'99, Lecture Notes in Computer Science. Springer-Verlag, March 1999.

35

Per Martin-Löf.
Constructive Mathematics and Computer Programming.
In Logic, Methodology and Philosophy of Science 6, pages 153-175, 1979.

36

William W. McCune.
OTTER Reference Manual and Guide.
Argonne National Laboratory, Illinois, USA, 3.0 edition, January 1994.

37

Robin Milner.
The use of machines to assist in rigorous proof, pages 77-88.
In Shepherdson and Hoare [53], March 1985.

38

Robin Milner, Mads Tofte, and Robert Harper.
The Definition of Standard ML.
MIT Press, March 1990.

39

Micha Muzalewski.
An Outline of PC Mizar.
Foundation of Logic, Mathematics and Informatics, Mizar User Group, Brussels, 1993.

40

Peter G. Neumann.
Computer-Related Risks.
Addison-Wesley, October 1994.

41

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.
Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science.
Springer, 2002.

42

M.A. Ozols, K.A. Eastaughffe, A. Cant, and S. Collignon.
DOVE: A tool for design modelling and verification in safety-critical systems.
In Proceedings of the 16th International System Safety Conference, Seattle, September 1998.

43

Lawrence C. Paulson.
The Foundation of a Generic Theorem Prover.
Journal of Automated Reasoning 5, pages 363-397, 1989.

44

Lawrence C. Paulson.
ML for the Working Programmer.
Cambridge University Press, second edition, June 1996.

45

Frank Pfenning and Carsten Schürmann.
System description: Twelf - a meta-logical framework for deductive systems.
In Harald Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, pages 202-206, Trento, Italy, July 1999. Springer-Verlag.
LNAI 1632.

46

Jenny Preece, Yvonne Rogers, Helen Sharp, David Benyon, Simon Holland, and Tom Carey.
Human-Computer Interaction, chapter 20.
In [47], 1994.

47

Jenny Preece, Yvonne Rogers, Helen Sharp, David Benyon, Simon Holland, and Tom Carey.
Human-Computer Interaction.
1994.

48

Christophe Raffalli and Paul Rozierè.
The PhoX Proof Checker Documentation.
Reference manual, LAMA, Laboratoire de Mathématiques, Université de Savoie and L'Equipe de Logique Mathématique, Université Paris 7, February 2003.
Version 0.83.

49

Eric Steven Raymond.
The Art of Unix Programming.
Addison-Wesley, September 2003.

50

B. Richie.
The design and implementation of an interactive proof editor.
PhD thesis, University of Edinburgh, November 1988.

51

Stephen R. Schach.
Classical and Object-Oriented Software Engineering: With UML and Java, chapter 15.
Computer Science Series. McGraw-Hill, fourth edition, 1999.

52

Helmut Schwichtenberg, editor.
Logic of Computation.
Springer, August 1997.

53

J.C. Shepherdson and C.A.R Hoare, editors.
Mathematical Logic and Programming Languages.
Prentice Hall, March 1985.

54

Ben Shneiderman.
Direct manipulation for comprehensible, predictable and controllable user interfaces.
In Intelligent User Interfaces, pages 33-39, January 1997.

55

Laurent Théry, Yves Bertot, and Gilles Kahn.
Real theorem provers deserve real user-interfaces.
Technical Report 1684, Institut National de Recherche en Informatique et en Automatique, May 1992.

56

L.S. van Benthem Jutting.
Checking Landau's "Grundlagen" in the Automath system.
PhD thesis, Technische Hogeschool Eindhoven, Stichting Mathematisch Centrum, 1977.
See also: [29].

57

Freek Wiedijk.
Mizar: An impression.
http://www.cs.kun.nl/~freek/mizar/index.html. Accessed June 2003, last modified January 2002.