Bibliography
These are some of the documents I have been reading during the year, in no particular order.
| [1] |
William W. McCune.
OTTER Reference Manual and Guide.
Argonne National Laboratory, Illinois, USA, 3.0 edition, January
1994. [ bib ] |
| [2] |
Michal Muzalewski.
An Outline of PC Mizar.
Foundation of Logic, Mathematics and Informatics, Mizar User Group,
Brussels, 1993. [ bib ] |
| [3] |
Freek Wiedijk.
Mizar: An impression. Accessed June 2003, last modified January 2002. [ bib | www ] |
| [4] |
Olivier Pons.
Undoing and managing a proof.
In Proceedings of Workshop on User Interfaces to Theorem
Provers, 1997. [ bib | .html ] |
| [5] |
Nicholas A. Merriam and Michael D. Harrison.
What is wrong with guis for theorem provers.
In Proceedings of User Interfaces for Theorem Provers, 1997. [ bib | .html ] |
| [6] |
Katherine A. Eastaughfee.
Support for interactive theorem proving: Some design principles and
their application, 1998. [ bib | .html ] |
| [7] |
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. [ bib ] |
| [8] |
Yves Bertot.
The CtCoq System: Design and Architecture.
Technical Report 3540, Institut National de Recherche en Informatique
et en Automatique, October 1998. [ bib ] |
| [9] |
Janet Bertot and Yves Bertot.
CtCoq: A system presentation.
In Wirsing and Nivat [10], pages 600-603.
LNCS. [ bib ] |
| [10] |
Martin Wirsing and Maurice Nivat, editors.
Algebraic Methodology and Software Technology, Munich, July
1996. Springer.
LNCS. [ bib ] |
| [11] |
B. Richie.
The design and implementation of an interactive proof editor.
PhD thesis, University of Edinburgh, November 1988. [ bib ] |
| [12] |
Luís Cruz-Filipe and Bas Spitters.
Program extraction from large proof developments.
In International Conference on Theorem Proving in Higher Order
Logics, 2003. [ bib ] |
| [13] |
Michael R.A. Huth and Mark D. Ryan.
Logic in Computer Science - Modelling and reasoning about
systems.
Cambridge University Press, 2000. [ bib | www ] |
| [14] |
M. Lowry, A. Philpot, T. Pressburger, and I. Underwood.
Amphion: Automatic Programming for Scientific Subroutine
Libraries, pages 326-335.
Volume 869 of Ras and Zemankova [15], October 1994. [ bib ] |
| [15] |
Zbigniew W. Ras and Maria Zemankova, editors.
Proceedings of the 8th International Symposium on Methodologies
for Intelligent Systems, volume 869 of LNCS.
Springer-Verlag, October 1994. [ bib ] |
| [16] |
W.A. Howard.
The formulae-as-types notion of construction, pages 479-490.
In Seldin and Hindley [17], 1980. [ bib ] |
| [17] |
J.R. Seldin and R.J. Hindley, editors.
To H.B. Curry: essays on combinatory logic, lambda calculus and
formalism.
Academic Press, London, New York, 1980. [ bib ] |
| [18] |
Alan Cooper.
About Face - The Essentials of User Interface Design.
IDG Books Worldwide, 1995. [ bib ] |
| [19] |
Constance Heitmeyer.
On the need for practical formal methods.
In A.P. Ravn and H. Rischel, editors, Formal Techniques in
Real-Time and Fault-Tolerant Systems, pages 18-26. Naval Research
Laboratory, Springer, September 1998. [ bib | www ] |
| [20] |
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. [ bib ] The significant intellectual cost of programming is for problem solving and explaining and not for coding. Yet, programming systems offer mechanical assistance exclusively with the coding process. Here we describe an implemented program development TR86-779 system, called PRL (pearl), that provides automated assistance with the hard part. The program and its explanation are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs. |
| [21] |
Laurence C. Paulson.
Isabelle: The next 700 theorem provers.
Technical Report TR-143, Computer Laboratory, University of
Cambridge, November 1989. [ bib | ftp ] |
| [22] |
Robert L. Constable.
The structure of Nuprl's type theory, pages 123-156.
In Schwichtenberg [23], August 1997. [ bib | www ] |
| [23] |
Helmut Schwichtenberg, editor.
Logic of Computation.
Springer, August 1997. [ bib ] |
| [24] |
James Caldwell.
Moving proofs-as-programs into practice.
In Proceedings, 12th IEEE International Conference Automated
Software Engineering, pages 10-17. IEEE Computer Society, 1997. [ bib | www ] |
| [25] |
Susumu Hayashi and Hiroshi Nakano.
PX: A Comuptational Logic.
MIT Press, 1988. [ bib | www] |
| [26] |
Christoph Kreitz.
Constructive automata theory implemented with the Nuprl proof
development system.
Technical Report TR86-779, Department of Computer Science, Cornell
University, Ithaca, New York, USA, September 1986. [ bib ] The Nuprl proof development system was designed for the computer-assisted problem solving in mathematics and programming. In particular it can be used for the development of mathematical proofs and of programs which are guaranteed to meet their specifications. The implementation of the theory of finite automata gave lots of insights into its strengths and weaknesses and shows that Nuprl is indeed powerful enough now to obtain nontrivial results within reasonable amounts of time. Its success shall encourage people to actually use the system and build theories within it.This report describes the techniques and the user-defined extensions to the Nuprl object language which were necessary to formulate and prove theorems from the theory of finite automata. It also describes the experiences which came from actually working with the current Nuprl system and gave some useful insights into its strenghts and weaknesses. A complete Nuprl-proof of the pumping lemma and its computational evaluation are presented and an outline for future development is given. |
| [27] |
Philip Wadler.
Proofs are programs.
November 2000. [ bib | www ] |
| [28] |
Lawrence C. Paulson.
The Foundation of a Generic Theorem Prover.
Journal of Automated Reasoning 5, pages 363-397, 1989. [ bib ] |
| [29] |
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. [ bib ] |
| [30] |
Per Martin-Löf.
Constructive Mathematics and Computer Programming.
In Logic, Methodology and Philosophy of Science 6, pages
153-175, 1979. [ bib ] |
| [31] |
David Albrecht and John N. Crossley.
Program extraction, simplified proof-terms and realizability.
Technical Report 271, Department of Computer Science, Monash
University, 1996. [ bib ] |
| [32] |
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. [ bib | www ] |
| [33] |
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. [ bib | www ] |
| [34] |
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. [ bib | www ] |
| [35] |
Iman Poernomo and John N. Crossley.
The curry-howard isomorphism adapted for imperitive program synthesis
and reasoning.
Technical report, School of Computer Science and Software
Engineering, Monash University. [ bib | www ] |
| [36] |
Edmund Yehezkel Landau.
Grundlagen der Analysis.
Erstveröff, Leipzig, first edition, 1930. [ bib ] |
| [37] |
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 [ bib | www] |
| [38] |
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. [ bib ] |
| [39] |
David Aspinall and Thomas Kleymann.
Adapting Proof General.
Laboratory for Foundations of Computer Science, Edinburgh, September
2002. [ bib | www ] |
| [40] |
David Aspinall.
Proof General Kit white paper, July 2003.
Laboratory for Foundations of Computer Science. [ bib | www ] |
| [41] |
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. [ bib | www ] |
| [42] |
M. J. C. Gordon and T. F. Melham, editors.
Introduction to HOL: A theorem proving environment for higher
order logic.
Cambridge University Press, 1993. [ bib | www ] |
| [43] |
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. [ bib | www ] |
| [44] |
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. [ bib | www ] |
| [45] |
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. [ bib | www ] |
| [46] |
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. [ bib | www ] |
| [47] |
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. [ bib | ftp ] |
| [48] |
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. [ bib ] |
| [49] |
Robin Milner.
The use of machines to assist in rigorous proof, pages 77-88.
In Shepherdson and Hoare [50], March 1985. [ bib ] |
| [50] |
J.C. Shepherdson and C.A.R Hoare, editors.
Mathematical Logic and Programming Languages.
Prentice Hall, March 1985. [ bib ] |
| [51] |
L.S. van Benthem Jutting.
Checking Landau's Grundlagen in the Automath system.
PhD thesis, Technische Hogeschool Eindhoven, Stichting Mathematisch
Centrum, 1977.
See also: [36]. [ bib | http ] |
| [52] |
Elliotte Rusty Harold and W. Scott Means.
XML in a Nutshell.
In a Nushell series. O'Reilly and Associates, second edition, June
2002. [ bib | www ] |
| [53] |
Bob Glickstein.
Writing GNU Emacs Extensions.
O'Reilly and Associates, April 1997. [ bib ] |
| [54] |
Lawrence C. Paulson.
ML for the Working Programmer.
Cambridge University Press, second edition, June 1996. [ bib ] |
| [55] |
Robin Milner, Mads Tofte, and Robert Harper.
The Definition of Standard ML.
MIT Press, March 1990. [ bib ] |
| [56] |
Walter F. Tichy.
RCS - a system for version control.
Software - Practice and Experience, 15(7):637-654, 1985. [ bib | www ] |
| [57] |
Don Bolinger and Tan Bronson.
Applying RCS and SCCS: From Source Control to Project Control.
O'Reilly and Associates, March 1995. [ bib | www ] |
| [58] |
Per Cederqvist et al.
Version Management with CVS (for CVS 1.11.6), 1993. [ bib | www ] |
| [59] |
Per Cederqvist et al.
Version Management with CVS (for CVS 1.12.1), 1993. [ bib | www ] |
| [60] |
Nancy Leveson.
An investigation of the Therac-25 accidents.
Technical Report 92-11-05, University of Washington, 1992. [ bib ] |
| [61] |
Peter G. Neumann.
Computer-Related Risks.
Addison-Wesley, October 1994. [ bib ] |
| [62] |
David Evans and David Larochelle.
Splint Manual.
Secure Programming Group, University of Virginia Department of
Computer Science, June 2003. [ bib | www ] |
| [63] |
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. [ bib | www ] |
| [64] |
Stephen R. Schach.
Classical and Object-Oriented Software Engineering: With UML and
Java, chapter 15.
Computer Science Series. McGraw-Hill, fourth edition, 1999. [ bib ] |
| [65] |
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. [ bib ] |
| [66] |
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. [ bib ] |
| [67] |
Anthony Cant and Mark Ozols.
XIsabelle: A Graphical User Interface to the Isabelle
Theorem Prover (draft).
Technical report. [ bib | ftp] |
| [68] |
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. [ bib ] |
| [69] |
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. [ bib ] |
| [70] |
Ben Collins-Sussman, Brian W. Fitzpatrick, and C. Michael Pilato.
Subversion: The definitive guide.
Draft Revision 6204:6215, May 2003. [ bib | www ] |
| [71] |
Ron Avitzur.
Direct manipulation in a mathematics user interface, pages
43-60.
In Kajler [72], January 1999. [ bib ] |
| [72] |
N. Kajler, editor.
Computer-Human Interaction in Symbolic Computation.
Springer, January 1999. [ bib ] |
| [73] |
Ben Shneiderman.
Direct manipulation for comprehensible, predictable and controllable
user interfaces.
In Intelligent User Interfaces, pages 33-39, January 1997. [ bib ] |
| [74] |
Clayton Lewis and Donald A. Norman.
Designing for Error, chapter 20.
In Norman and Draper [75], 1986. [ bib ] |
| [75] |
Donald A. Norman and Stephen W. Draper, editors.
User Centered Design.
Lawrence Erlbaum Associates, 1986. [ bib ] |
| [76] |
Jenny Preece, Yvonne Rogers, Helen Sharp, David Benyon, Simon Holland, and Tom
Carey.
Human-Computer Interaction, chapter 20.
In [77], 1994. [ bib ] |
| [77] |
Jenny Preece, Yvonne Rogers, Helen Sharp, David Benyon, Simon Holland, and Tom
Carey.
Human-Computer Interaction.
1994. [ bib ] |
| [78] |
RELAX NG Specification, December 2001. [ bib | ] |
| [79] |
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. [ bib | www ] |
| [80] |
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. [ bib | www ] |
| [81] |
Eric Steven Raymond.
The Art of Unix Programming.
Addison-Wesley, September 2003. [ bib ] |