thesisbib.bib

@MANUAL{otter,
  TITLE = {OTTER Reference Manual and Guide},
  AUTHOR = {William W. McCune},
  ORGANIZATION = {Argonne National Laboratory},
  ADDRESS = {Illinois, USA},
  EDITION = {3.0},
  YEAR = {1994},
  MONTH = {January},
  FILE = {/home/mostynm/papers/otter3_manual.ps.gz}
}

@MANUAL{mizar_man,
  TITLE = {An Outline of PC Mizar},
  AUTHOR = {Micha{\l} Muzalewski},
  EDITOR = {Roman Matuszewski},
  YEAR = {1993},
  ADDRESS = {Brussels},
  ORGANIZATION = {Foundation of Logic, Mathematics and Informatics, 
		Mizar User Group},
  FILE = {/home/mostynm/papers/mizarmanual.ps.gz}
}

@UNPUBLISHED{mizar_intro,
  TITLE = {Mizar: An Impression},
  AUTHOR = {Freek Wiedijk},
  NOTE = {\url{http://www.cs.kun.nl/~freek/mizar/index.html}. 
		Accessed June 2003, last modified January 2002},
  FILE = {/home/mostynm/papers/mizarintro.ps.gz}
}

@INPROCEEDINGS{pons97undoing,
  AUTHOR = {Olivier Pons},
  TITLE = {Undoing and Managing a proof},
  BOOKTITLE = {Proceedings of Workshop on User Interfaces to Theorem Provers},
  YEAR = {1997},
  URL = {\url{http://citeseer.nj.nec.com/pons97undoing.html}},
  FILE = {/home/mostynm/papers/pons97undoing.ps.gz}
}

@INPROCEEDINGS{merriam97what,
  AUTHOR = {Nicholas A. Merriam and Michael D. Harrison},
  TITLE = {What is wrong with GUIs for theorem provers},
  BOOKTITLE = {Proceedings of User Interfaces for Theorem Provers},
  YEAR = {1997},
  FILE = {/home/mostynm/papers/merriam97what.ps.gz},
  URL = {\url{http://citeseer.nj.nec.com/merriam97what.html}}
}

@MISC{eastaughoee98support,
  AUTHOR = {Katherine A. Eastaughfee},
  TITLE = {Support for interactive theorem proving: Some design principles 
		and their application},
  TEXT = {Katherine Eastaughfee. Support for interactive theorem proving: 
		Some design principles and their application. In Informal Proceedings 
		of User Interfaces for Theorem Provers 1998, 
		Eindhoven University of Technology, 1998. RR n# 3540 24 Yves Bertot},
  YEAR = {1998},
  FILE = {/home/mostynm/papers/support-for-interactive-theorem.ps.gz},
  URL = {\url{http://citeseer.nj.nec.com/14431.html}}
}

@TECHREPORT{real-interfaces,
  AUTHOR = {Laurent Th\'ery and Yves Bertot and Gilles Kahn},
  TITLE = {Real Theorem Provers Deserve Real User-Interfaces},
  INSTITUTION = {Institut National de Recherche en Informatique et en Automatique},
  NUMBER = {1684},
  YEAR = {1992},
  MONTH = {May},
  FILE = {/home/mostynm/papers/sde5.ps}
}

@TECHREPORT{ctcoq,
  AUTHOR = {Yves Bertot},
  TITLE = {The {CtCoq} {S}ystem: {D}esign and {A}rchitecture},
  YEAR = {1998},
  MONTH = {October},
  NUMBER = {3540},
  INSTITUTION = {Institut National de Recherche en Informatique et en Automatique},
  FILE = {/home/mostynm/papers/RR-3540.ps.gz}
}

@INPROCEEDINGS{bertot96ctcoq,
  AUTHOR = {Janet Bertot and Yves Bertot},
  TITLE = {Ct{C}oq: A System Presentation},
  BOOKTITLE = {Algebraic Methodology and Software Technology},
  PAGES = {600--603},
  YEAR = {1996},
  CROSSREF = {amast96},
  FILE = {/home/mostynm/papers/bertot96ctcoq.pdf}
}

@PROCEEDINGS{amast96,
  TITLE = {Algebraic Methodology and Software Technology},
  YEAR = {1996},
  MONTH = {July},
  EDITOR = {Martin Wirsing and Maurice Nivat},
  PUBLISHER = {Springer},
  ADDRESS = {Munich},
  NOTE = {LNCS},
  ISBN = {3-540-61463-X}
}

@PHDTHESIS{pbp,
  AUTHOR = {B. Richie},
  TITLE = {The design and implementation of an interactive proof editor},
  SCHOOL = {University of Edinburgh},
  MONTH = {November},
  YEAR = {1988}
}

@CONFERENCE{pelpd,
  AUTHOR = {Lu\'is Cruz-Filipe and Bas Spitters},
  TITLE = {Program extraction from large proof developments},
  BOOKTITLE = {International Conference on Theorem Proving in Higher Order Logics},
  YEAR = {2003},
  FILE = {/home/mostynm/papers/paper3.pdf}
}

@BOOK{logic-in-cs,
  AUTHOR = {Michael R.A. Huth and Mark D. Ryan},
  TITLE = {Logic in Computer Science -- Modelling and reasoning about systems},
  PUBLISHER = {Cambridge University Press},
  YEAR = {2000},
  ISBN = {0521656028},
  URL = {\url{http://www.cs.bham.ac.uk/research/lics/}}
}

@INBOOK{amphion,
  AUTHOR = {M. Lowry and A. Philpot and T. Pressburger and I. Underwood},
  TITLE = {Amphion: Automatic Programming for Scientific Subroutine 
		Libraries},
  ORGANISATION = {NASA},
  ADDRESS = {Charlotte, North Carolina},
  PAGES = {326--335},
  CROSSREF = {mis94}
}

@BOOK{mis94,
  TITLE = {Proceedings of the 8th International Symposium on 
		Methodologies for Intelligent Systems},
  EDITOR = {Zbigniew W. Ras and Maria Zemankova},
  PUBLISHER = {Springer-Verlag},
  YEAR = {1994},
  MONTH = {October},
  VOLUME = {869},
  SERIES = {LNCS}
}

@INBOOK{curry-howard,
  AUTHOR = {W.A. Howard},
  TITLE = {The formulae-as-types notion of construction},
  PAGES = {479--490},
  CROSSREF = {to_hb_curry}
}

@BOOK{to_hb_curry,
  TITLE = {To H.B. Curry: essays on combinatory logic, lambda calculus
		and formalism},
  EDITOR = {J.R. Seldin and R.J. Hindley},
  PUBLISHER = {Academic Press},
  ADDRESS = {London, New York},
  YEAR = {1980}
}

@BOOK{about-face,
  AUTHOR = {Alan Cooper},
  TITLE = {About Face - The Essentials of User Interface Design},
  ISBN = {1-56884-322-4},
  PUBLISHER = {IDG Books Worldwide},
  YEAR = {1995}
}

@INPROCEEDINGS{formal-techniques,
  AUTHOR = {Constance Heitmeyer},
  ORGANIZATION = {Naval Research Laboratory},
  TITLE = {On the Need for \begin{em}Practical\end{em} Formal Methods},
  BOOKTITLE = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
  EDITOR = {A.P. Ravn and H. Rischel},
  PAGES = {18--26},
  YEAR = {1998},
  MONTH = {September},
  PUBLISHER = {Springer},
  URL = {\url{http://link.springer.de/link/service/series/0558/tocs/t1486.htm}},
  FILE = {/home/mostynm/papers/1998heitmeyer-FTRTFT98.pdf}
}

@TECHREPORT{proofs-as-programs,
  AUTHOR = {Joseph L. Bates and Robert L. Constable},
  TITLE = {{P}roofs as {P}rograms},
  ABSTRACT = {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.},
  MONTH = {February},
  YEAR = {1983},
  NUMBER = {82-530},
  INSTITUTION = {Department of Computer Science, Cornell University},
  ADDRESS = {Ithaca, New York, USA},
  FILE = {/home/mostynm/papers/TR82-530.ps.gz}
}

@TECHREPORT{next700,
  AUTHOR = {Laurence C. Paulson},
  TITLE = {Isabelle: The Next 700 Theorem Provers},
  INSTITUTION = {Computer Laboratory, University of Cambridge},
  NUMBER = {TR-143},
  MONTH = {November},
  YEAR = {1989},
  URL = {\url{ftp://ftp.cl.cam.ac.uk/papers/reports/TR143-lcp-experience.dvi.gz}},
  FILE = {/home/mostynm/papers/TR143-lcp-experience.pdf}
}

@INBOOK{constable97structure,
  AUTHOR = {Robert L. Constable},
  TITLE = {The structure of Nuprl's type theory},
  PAGES = {123--156},
  FILE = {/home/mostynm/papers/constable97structure.ps.gz},
  CROSSREF = {logicofcomputation},
  URL = {\url{http://citeseer.nj.nec.com/constable97structure.html}}
}

@BOOK{logicofcomputation,
  TITLE = {Logic of Computation},
  EDITOR = {Helmut Schwichtenberg},
  PUBLISHER = {Springer},
  YEAR = {1997},
  MONTH = {August},
  ISBN = {3540629637}
}

@INPROCEEDINGS{caldwell97,
  AUTHOR = {James Caldwell},
  TITLE = {Moving Proofs-as-Programs into Practice},
  BOOKTITLE = {Proceedings, 12th IEEE International Conference Automated 
		Software Engineering},
  YEAR = {1997},
  PAGES = {10--17},
  PUBLISHER = {IEEE Computer Society},
  FILE = {/home/mostynm/papers/caldwell97moving.ps.gz},
  URL = {\url{http://citeseer.nj.nec.com/caldwell97moving.html}}
}

@BOOK{px,
  AUTHOR = {Susumu Hayashi and Hiroshi Nakano},
  TITLE = {PX: A Comuptational Logic},
  PUBLISHER = {MIT Press},
  YEAR = {1988},
  NOTE = {\url{http://www602.math.ryukoku.ac.jp/~nakano/papers/freePXbook.pdf}},
  FILE = {/home/mostynm/papers/freePXbook.pdf}
}

@TECHREPORT{TR86-779,
  TITLE = {Constructive Automata Theory Implemented with the {N}uprl Proof Development System},
  AUTHOR = {Christoph Kreitz},
  ABSTRACT = { 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.},
  MONTH = {September},
  YEAR = {1986},
  NUMBER = {TR86-779},
  INSTITUTION = {Department of Computer Science, Cornell University},
  ADDRESS = {Ithaca, New York, USA},
  FILE = {/home/mostynm/papers/TR86-779.ps}
}

@ARTICLE{frege,
  AUTHOR = {Philip Wadler},
  TITLE = {Proofs are Programs},
  MONTH = {November},
  YEAR = {2000},
  INSTITUTION = {Avaya Labs},
  URL = {\url{http://www.research.avayalabs.com/user/wadler/papers/frege/frege.pdf}},
  FILE = {/home/mostynm/papers/frege.pdf}
}

@ARTICLE{TR130,
  AUTHOR = {Lawrence C. Paulson},
  TITLE = {{T}he {F}oundation of a {G}eneric {T}heorem {P}rover},
  JOURNAL = {Journal of Automated Reasoning 5},
  YEAR = {1989},
  PAGES = {363-397},
  INSTITUTION = {University of Cambridge},
  FILE = {/home/mostynm/papers/TR130-lcp-generic-theorem-prover.pdf}
}

@BOOK{isabelle,
  AUTHOR = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  TITLE = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2283,
  YEAR = {2002}
}

@INPROCEEDINGS{Martin-Lof_Constructive_Math,
  AUTHOR = {Per Martin-L\"of},
  TITLE = {{C}onstructive {M}athematics and {C}omputer {P}rogramming},
  BOOKTITLE = {Logic, Methodology and Philosophy of Science 6},
  YEAR = {1979},
  PAGES = {153--175}
}

@TECHREPORT{Albrecht-Crossley_Program_extraction,
  AUTHOR = {David Albrecht and John N. Crossley},
  TITLE = {Program extraction, simplified proof-terms and realizability},
  INSTITUTION = {Department of Computer Science, Monash University},
  YEAR = {1996},
  NUMBER = {271},
  FILE = {/home/mostynm/papers/tr-cs96-271.ps.gz}
}

@ARTICLE{real-programs-from-real-proofs,
  AUTHOR = {John N. Crossley and Iman Poernomo},
  TITLE = {Fred: {A}n {A}pproach to {G}enerating {R}eal, {C}orrect, 
		{R}eusable {P}rograms from {P}roofs},
  JOURNAL = {Journal for Universal Computer Science (Online Edition)},
  YEAR = {2001},
  VOLUME = {7},
  NUMBER = {1},
  PAGES = {71--88},
  URL = {\url{http://www.jucs.org/jucs_7_1/}}
}

@TECHREPORT{coq,
  TITLE = {The {C}oq {P}roof {A}ssistant {R}eference {M}anual -- 
		{V}ersion 7.2},
  AUTHOR = {B. Barras and S. Boutin and C. Cornes and J. Courant 
		and J.C. Filliatre and E. Gim\'enez and H. Herbelin
		and G. Huet and C. Mu{\~n}oz and C. Murthy and C. Parent 
		and C. Paulin and A. Sa\"{\i}bi and B. Werner},
  INSTITUTION = {Institut National de Recherche en Informatique et en Automatique},
  MONTH = {February},
  YEAR = {2002},
  NUMBER = {0255},
  URL = {\url{http://pauillac.inria.fr/coq/doc/main.html}},
  FILE = {ftp://ftp.inria.fr/INRIA/coq/current/doc}
}

@TECHREPORT{pcoq,
  AUTHOR = {Ahmed Amerkad and Yves Bertot and Lo\"ic Pottier and 
		Laurence Rideau},
  TITLE = {Mathematics and Proof Presentation in {P}coq},
  INSTITUTION = {Institut National de Recherche en Informatique et en 
		Automatique},
  YEAR = {2001},
  MONTH = {November},
  URL = {\url{http://www-sop.inria.fr/lemme/pcoq/}},
  FILE = {/home/mostynm/papers/RR-4313.ps.gz}
}

@TECHREPORT{ch-iso,
  AUTHOR = {Iman Poernomo and John N. Crossley},
  TITLE = {The Curry-Howard isomorphism adapted for imperitive program 
		synthesis and reasoning},
  INSTITUTION = {School of Computer Science and Software Engineering, 
		Monash University},
  URL = {\url{http://www.csse.monash.edu.au/cgi-bin/pub_search?++crossley+}},
  FILE = {/home/mostynm/papers/tr-2002-117-full.ps}
}

@BOOK{landau-foundations-of-analysis,
  AUTHOR = {Edmund Yehezkel Landau},
  TITLE = {Grundlagen der Analysis},
  PUBLISHER = {Erstver\"off},
  ADDRESS = {Leipzig},
  YEAR = {1930},
  EDITION = {First},
  ISBN = {0828400792},
  FILE = {/home/mostynm/papers/grundlagen.ps.gz}
}

@CONFERENCE{eproof,
  AUTHOR = {David Aspinall},
  TITLE = {{P}rotocols for {I}nteractive e-{P}roof},
  BOOKTITLE = {13th International Conference on Theorem Proving in Higher
        Order Logics},
  YEAR = {2000},
  MONTH = {May},
  ORGANIZATION = {Laboratory for Foundations of Computer Science},
  NOTE = {Draft extended abstract, presented as a work-in-progress, 
		available from \url{http://homepages.inf.ed.ac.uk/da/papers/drafts/#eproof}},
  FILE = {/home/mostynm/papers/eproof.ps.gz}
}

@INPROCEEDINGS{proofgeneral,
  AUTHOR = {David Aspinall},
  TITLE = {{P}roof {G}eneral: A Generic Tool for Proof Development},
  ORGANIZATION = {Laboratory for Foundations of Computer Science},
  YEAR = {2000},
  BOOKTITLE = {Tools and Algorithms for the Construction and Analysis},
  PUBLISHER = {Springer},
  PAGES = {38--42},
  NOTE = {LNCS 1785},
  FILE = {/home/mostynm/papers/pgoutline.ps.gz}
}

@MANUAL{adapting_proofgeneral,
  AUTHOR = {David Aspinall and Thomas Kleymann},
  TITLE = {Adapting Proof General},
  ORGANIZATION = {Laboratory for Foundations of Computer Science},
  ADDRESS = {Edinburgh},
  YEAR = {2002},
  MONTH = {September},
  NOTE = {\url{http://proofgeneral.inf.ed.ac.uk/}}
}

@MISC{pgkit,
  AUTHOR = {David Aspinall},
  TITLE = {{P}roof {G}eneral {K}it White Paper},
  YEAR = {2003},
  MONTH = {July},
  ORGANIZATION = {Laboratory for Foundations of Computer Science},
  NOTE = {Laboratory for Foundations of Computer Science, 
		\url{http://homepages.inf.ed.ac.uk/da/papers/drafts/#white}},
  FILE = {/home/mostynm/papers/white.ps.gz}
}

@INPROCEEDINGS{twelf,
  AUTHOR = {Frank Pfenning and Carsten Sch\"urmann},
  TITLE = {System description: Twelf -- A Meta-Logical Framework for 
		Deductive Systems},
  BOOKTITLE = {Proceedings of the 16th International Conference on 
		Automated Deduction},
  YEAR = {1999},
  EDITOR = {Harald Ganzinger},
  MONTH = {July},
  PUBLISHER = {Springer-Verlag},
  NOTE = {LNAI 1632},
  ADDRESS = {Trento, Italy},
  PAGES = {202--206},
  FILE = {/home/mostynm/papers/cade99.ps.gz},
  URL = {\url{http://www.cs.cmu.edu/~twelf}}
}

@BOOK{hol,
  EDITOR = {M. J. C. Gordon and T. F. Melham},
  TITLE = {Introduction to HOL: A theorem proving environment for 
		higher order logic},
  YEAR = {1993},
  PUBLISHER = {Cambridge University Press},
  ISBN = {0 521 44189 7},
  URL = {\url{http://www.dcs.gla.ac.uk/\~tfm/Papers/HOLbook.html}}
}

@ARTICLE{acl2,
  TITLE = {An Industrial Strength Theorem Prover for a Logic Based on 
		{C}ommon {L}isp},
  AUTHOR = {Matt Kaufmann and J. Moore},
  JOURNAL = {IEEE Transactions on Software Engineering},
  VOLUME = {23},
  NUMBER = {4},
  PAGES = {203--213},
  YEAR = {1997},
  MONTH = {April},
  URL = {\url{http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html}},
  FILE = {/home/mostynm/papers/km97.ps.Z}
}

@ARTICLE{plastic,
  TITLE = {An Implementation of {LF} with Coercive Subtyping & Universes},
  AUTHOR = {P. Callaghan and Z. Luo},
  JOURNAL = {Journal of Automated Reasoning},
  VOLUME = {27},
  NUMBER = {1},
  MONTH = {July},
  PAGES = {3--27},
  YEAR = {2000},
  NOTE = {Special Issue on Logical Frameworks and Metalanguages},
  URL = {\url{http://www.dur.ac.uk/CARG/publications.html#lf_cs_u}}
}

@TECHREPORT{phox,
  TITLE = {The {P}ho{X} {P}roof {C}hecker {D}ocumentation},
  AUTHOR = {Christophe Raffalli and Paul Rozier\`e},
  INSTITUTION = {LAMA, Laboratoire de Math\'ematiques, 
		Universit\'e de Savoie and L'Equipe de Logique Math\'ematique, 
		Universit\'e Paris 7},
  YEAR = {2003},
  MONTH = {February},
  TYPE = {Reference Manual},
  NOTE = {Version 0.83},
  FILE = {/home/mostynm/papers/phox.doc.ps.gz},
  URL = {\url{http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/phox.html#information}}
}

@TECHREPORT{lego,
  AUTHOR = {Zhaohui Luo and Randy Pollack},
  TITLE = {{LEGO} {P}roof {D}evelopment {S}ystem: {U}ser's {M}anual},
  YEAR = {1992},
  NUMBER = {ECS-LFCS-92-211},
  INSTITUTION = {School of Informatics, University of Edinburgh},
  FILE = {/home/mostynm/manual92.dvi.Z},
  URL = {\url{http://www.dcs.ed.ac.uk/home/lego/html/papers.html}}
}

@INPROCEEDINGS{proof-by-pointing,
  AUTHOR = {Yves Bertot and Gilles Kahn and Laurent Th\'ery},
  TITLE = {{P}roof by {P}ointing},
  MONTH = {April},
  YEAR = {1994},
  ISBN = {0387578870},
  BOOKTITLE = {Theoretical Aspects of Computer Software},
  PAGES = {141-160},
  VOLUME = {789},
  PUBLISHER = {Springer Verlag},
  FILE = {/home/mostynm/papers/pbp.ps},
  URL = {\url{ftp://ftp-sop.inria.fr/pub/centaur/papers/pbp.ps}}
}

@INCOLLECTION{Bruijn83,
  AUTHOR = {N.G. de Bruijn},
  TITLE = {{AUTOMATH}, a {L}anguage for {M}athematics},
  YEAR = {1983},
  BOOKTITLE = {Automation of Reasoning 2: Classical Papers on 
		Computational Logic 1967-1970},
  EDITOR = {J. Siekmann and G. Wrightson},
  PUBLISHER = {Springer},
  ADDRESS = {Berlin, Heidelberg},
  PAGES = {159--200}
}

@INBOOK{lcf,
  AUTHOR = {Robin Milner},
  TITLE = {The use of machines to assist in rigorous proof},
  PAGES = {77--88},
  CROSSREF = {mlpl}
}

@BOOK{mlpl,
  TITLE = {Mathematical Logic and Programming Languages},
  EDITOR = {J.C. Shepherdson and C.A.R Hoare},
  PUBLISHER = {Prentice Hall},
  MONTH = {March},
  YEAR = {1985}
}

@PHDTHESIS{jutting,
  AUTHOR = {L.S. van Benthem Jutting},
  TITLE = {Checking Landau's "Grundlagen" in the Automath system},
  YEAR = {1977},
  SCHOOL = {Technische Hogeschool Eindhoven, Stichting Mathematisch Centrum},
  URL = {\url{http://library.tue.nl/}},
  NOTE = {See also: \cite{landau-foundations-of-analysis}},
  FILE = {/home/mostynm/papers/7701940.pdf}
}

@BOOK{xmlnutshell,
  AUTHOR = {Elliotte Rusty Harold and W. Scott Means},
  TITLE = {XML in a Nutshell},
  MONTH = {June},
  YEAR = {2002},
  EDITION = {Second},
  PUBLISHER = {O'Reilly and Associates},
  SERIES = {In a Nushell series},
  URL = {\url{http://www.oreilly.com/catalog/xmlnut2/}}
}

@BOOK{emacs_extensions,
  AUTHOR = {Bob Glickstein},
  TITLE = {Writing GNU Emacs Extensions},
  MONTH = {April},
  YEAR = {1997},
  PUBLISHER = {O'Reilly and Associates}
}

@BOOK{ml_working_programmer,
  TITLE = {ML for the Working Programmer},
  AUTHOR = {Lawrence C. Paulson},
  EDITION = {Second},
  MONTH = {June},
  YEAR = {1996},
  PUBLISHER = {Cambridge University Press},
  ASIN = {0521570506}
}

@BOOK{ml_definition,
  TITLE = {The Definition of Standard ML},
  AUTHOR = {Robin Milner and Mads Tofte and Robert Harper},
  PUBLISHER = {MIT Press},
  YEAR = {1990},
  MONTH = {March},
  ASIN = {0262631326}
}

@ARTICLE{rcs,
  AUTHOR = {Walter F. Tichy},
  TITLE = {{RCS} -- A System for Version Control},
  JOURNAL = {Software -- Practice and Experience},
  VOLUME = {15},
  NUMBER = {7},
  PAGES = {637--654},
  YEAR = {1985},
  URL = {\url{http://citeseer.nj.nec.com/tichy91rcs.html}}
}

@BOOK{rcs_sccs,
  AUTHOR = {Don Bolinger and Tan Bronson},
  TITLE = {Applying RCS and SCCS: From Source Control to Project Control},
  PUBLISHER = {O'Reilly and Associates},
  MONTH = {March},
  YEAR = {1995},
  URL = {\url{http://www.oreilly.com/catalog/rcs/}}
}

@MANUAL{cvs_stable,
  AUTHOR = {Per Cederqvist et al},
  TITLE = {Version Management with CVS (for CVS 1.11.6)},
  YEAR = {1993},
  URL = {\url{http://www.cvshome.org/docs/manual/}}
}

@MANUAL{cvs_feature,
  AUTHOR = {Per Cederqvist et al},
  TITLE = {Version Management with CVS (for CVS 1.12.1)},
  YEAR = {1993},
  NOTE = {\url{http://www.cvshome.org/docs/manual/}}
}

@TECHREPORT{therac,
  AUTHOR = {Nancy Leveson},
  TITLE = {An investigation of the {T}herac-25 accidents},
  INSTITUTION = {University of Washington},
  YEAR = {1992},
  NUMBER = {92-11-05}
}

@BOOK{risks,
  AUTHOR = {Peter G. Neumann},
  TITLE = {Computer-Related Risks},
  PUBLISHER = {Addison-Wesley},
  ISBN = {0-201-55805-X},
  YEAR = {1994},
  MONTH = {October}
}

@MANUAL{splint_man,
  TITLE = {Splint Manual},
  AUTHOR = {David Evans and David Larochelle},
  ORGANIZATION = {Secure Programming Group, 
		University of Virginia Department of Computer Science},
  MONTH = {June},
  YEAR = {2003},
  VERSION = {version 3.1.1-1},
  NOTE = {\url{http://lclint.cs.virginia.edu/manual/}}
}

@INPROCEEDINGS{splint,
  TITLE = {Statically Detecting Likely Buffer Overflow Vulnerabilities},
  AUTHOR = {David Larochelle and David Evans},
  ORGANIZATION = {University of Virginia, Department of Computer Science},
  BOOKTITLE = {10th USENIX Security Symposium},
  PUBLISHER = {USENIX Association},
  PAGES = {177--190},
  MONTH = {August},
  YEAR = {2001},
  URL = {\url{http://www.usenix.org/events/sec01/larochelle.html}}
}

@INBOOK{coose,
  TITLE = {Classical and Object-Oriented Software Engineering: 
		With UML and Java},
  AUTHOR = {Stephen R. Schach},
  CHAPTER = {15},
  PUBLISHER = {McGraw-Hill},
  YEAR = {1999},
  ISBN = {0-07-230227-5},
  SERIES = {Computer Science Series},
  EDITION = {fourth}
}

@INPROCEEDINGS{holloway,
  TITLE = {Why Engineers Should Consider Formal Methods},
  AUTHOR = {C. Michael Holloway},
  YEAR = {1997},
  MONTH = {October},
  PAGES = {7},
  BOOKTITLE = {Proceedings of the 16th AIAA/IEEE Digital Avionics Systems 
		Conference},
  ORGANIZATION = {NASA Langley Research Center},
  FILE = {/home/mostynm/papers/NASA-97-16dasc-cmh.pdf}
}

@CONFERENCE{notwidely,
  AUTHOR = {John C. Knight and Colleen L. DeJong and Matthew S. Gribble 
		and Lu\'is G. Nakano},
  TITLE = {{W}hy {A}re {F}ormal {M}ethods {N}ot {U}sed {M}ore {W}idely?},
  BOOKTITLE = {Fourth NASA Formal Methods Workshop},
  YEAR = {1997},
  MONTH = {September},
  ORGANIZATION = {University of Virginia, Department of Computer Science},
  FILE = {/home/mostynm/papers/lfm.97.pdf}
}

@TECHREPORT{xisabelle,
  AUTHOR = {Anthony Cant and Mark Ozols},
  TITLE = {{XIsabelle}: {A} {G}raphical {U}ser {I}nterface to the {I}sabelle 
		{T}heorem {P}rover (draft)},
  ORGANIZATION = {Information Technology Division, DSTO},
  NOTE = {Available from \url{ftp://ftp.cl.cam.ac.uk/ml/}},
  FILE = {/home/mostynm/papers/XIsabelle.ps.gz}
}

@INPROCEEDINGS{dove,
  TITLE = {{DOVE}: A Tool for Design Modelling and Verification in 
		Safety-Critical Systems},
  AUTHOR = {M.A. Ozols and K.A. Eastaughffe and A. Cant and S. Collignon},
  BOOKTITLE = {Proceedings of the 16th International System Safety 
		Conference},
  MONTH = {September},
  YEAR = {1998},
  ADDRESS = {Seattle},
  FILE = {/home/mostynm/papers/dove.pdf}
}

@INPROCEEDINGS{isawin,
  AUTHOR = {C. L\"uth and H. Tej and Kolyang, B. Krieg-Br\"uckner},
  TITLE = {{TAS} and {I}sa{W}in: {T}ools for {T}ransformational {P}rogram 
		{D}evelopment and {T}heorem {P}roving},
  BOOKTITLE = {{E}uropean {J}oint {C}onference on {T}heory and 
		{P}ractice of {S}oftware {ETAPS}'99},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  YEAR = {1999},
  MONTH = {March},
  FILE = {/home/mostynm/papers/etaps99_sysdesc.ps.gz}
}

@UNPUBLISHED{subversion,
  TITLE = {Subversion: The Definitive Guide},
  AUTHOR = {Ben Collins-Sussman and Brian W. Fitzpatrick and 
		C. Michael Pilato},
  NOTE = {Draft Revision 6204:6215, available at 
		\url{http://svnbook.red-bean.com/}},
  YEAR = {2003},
  MONTH = {May}
}

@INBOOK{gcalc,
  AUTHOR = {Ron Avitzur},
  TITLE = {Direct manipulation in a mathematics user interface},
  PAGES = {43--60},
  CROSSREF = {chisc}
}

@BOOK{chisc,
  TITLE = {Computer-Human Interaction in Symbolic Computation},
  EDITOR = {N. Kajler},
  PUBLISHER = {Springer},
  YEAR = {1999},
  MONTH = {January},
  ISBN = {3-211-82843-5}
}

@INPROCEEDINGS{shneiderman97direct,
  AUTHOR = {Ben Shneiderman},
  TITLE = {Direct Manipulation for Comprehensible, Predictable and 
		Controllable User Interfaces},
  BOOKTITLE = {Intelligent User Interfaces},
  PAGES = {33--39},
  YEAR = {1997},
  MONTH = {January},
  FILE = {/home/mostynm/papers/shneiderman97direct.ps.gz}
}

@INBOOK{designingforerror,
  TITLE = {Designing for Error},
  AUTHOR = {Clayton Lewis and Donald A. Norman},
  CHAPTER = {20},
  CROSSREF = {usercentered}
}

@BOOK{usercentered,
  TITLE = {User Centered Design},
  EDITOR = {Donald A. Norman and Stephen W. Draper},
  PUBLISHER = {Lawrence Erlbaum Associates},
  YEAR = {1986},
  ISBN = {0-89859-872-9}
}

@INBOOK{task_analysis,
  CHAPTER = {20},
  CROSSREF = {preece_hci}
}

@BOOK{preece_hci,
  TITLE = {Human-Computer Interaction},
  AUTHOR = {Jenny Preece and Yvonne Rogers and Helen Sharp and David Benyon 
		and Simon Holland and Tom Carey},
  PUBLICHER = {Addison-Wesley},
  YEAR = {1994},
  ISBN = {0-20162-769-8}
}

@MISC{relaxng,
  TITLE = {{RELAX NG} {S}pecification},
  EDITOR = {James Clark and MURATA Makoto},
  MONTH = {December},
  YEAR = {2001},
  NOTE = {Available from \url{http://www.relaxng.org/spec-20011203.html}}
}

@ARTICLE{openmath,
  AUTHOR = {John Abbott and Angel D{\'\i}az and Robert S. Sutor},
  TITLE = {A report on {OpenMath}. {A} protocol for the exchange of 
		mathematical information},
  JOURNAL = {SIGSAM Bulletin (ACM Special Interest Group on Symbolic 
		and Algebraic Manipulation)},
  VOLUME = {30},
  NUMBER = {1},
  PAGES = {21--24},
  YEAR = {1996},
  URL = {\url{http://citeseer.nj.nec.com/abbott96report.html}},
  FILE = {/home/mostynm/abbott96report.ps.gz}
}

@TECHREPORT{mathml,
  TITLE = {{M}athematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0},
  INSTITUTION = {{W}orld {W}ide {W}eb {C}onsortium},
  YEAR = {2000},
  MONTH = {March},
  AUTHOR = {Ron Ausbrooks and Stephen Buswell and St\'ephane Dalmas 
		and Stan Devitt and Angel Diaz and Roger Hunter and Bruce Smith 
		and Neil Soiffer and Robert Sutor and Stephen Watt},
  NOTE = {Edited by Nico Poppelier, Robert Miner, Patrick Ion 
		and David Carlisle. 
		Available from \url{http://www.w3.org/TR/MathML2/}},
  FILE = {/home/mostynm/papers/PDF-p-MathML-20000328.pdf}
}

@BOOK{taoup,
  TITLE = {The Art of Unix Programming},
  AUTHOR = {Eric Steven Raymond},
  YEAR = {2003},
  PUBLISHER = {Addison-Wesley},
  MONTH = {September},
  ISBN = {0131429019}
}