@incollection{bruijn80,
  author    = {Nicolaas Govert de Bruijn},
  title     = {A Survey of the Project {AUTOMATH}},
  editor    = {J.P. Seldin and J. R. Hindley},
  booktitle = {To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus
               and Formalism},
  publisher = {Academic Press},
  year      = {1980},
  pages     = {579--606}}

@book         {church41,
  author    = {A. Church},
  title     = {The Calculi of Lambda-Conversion},
  publisher = {Princeton University Press},
  year      = {1941}}

@book         {constable86,
  author    = {Robert L. Constable and S. Allen and H. Bromly and
               W. Cleaveland and J. Cremer and R. Harper and D. Howe and
               T. Knoblock and N. Mendler and P. Panangaden and J. Sasaki and
               S. Smith},
  title     = {Implementing Mathematics with the Nuprl Proof Development 
               System},
  publisher = {Prentice-Hall},
  address   = {Englewood Cliffs, New Jersey},
  year      = {1986}}

@inproceedings{dobbertin96,
  author    = {Hans Dobbertin and Antoon Bosselaers and Bart Preneel},
  title     = {{RIPEMD}-160: A Strengthened Version of {RIPEMD}},
  booktitle = {Fast Software Encryption},
  pages     = {71-82},
  year      = {1996},
  note      = {\url{http://citeseer.nj.nec.com/dobbertin96ripemd.html}}}

@article      {godel31,
  author    = {K. G{\"o}del},
  title     = {{\"U}ber for\-mal un\-ent\-scheid\-ba\-re
               {S\"at}\-ze der {Prin}\-ci\-pia 
               {Mathe}\-ma\-ti\-ca und ver\-wand\-ter
               {Sys}\-teme {I}},
  journal   = {Mo\-nats\-hef\-te f{\"u}r {Mathe}\-ma\-tik und {Phy}\-sik},
  year      = {19\-31},
  volume    = {12},
  number    = {{XXXVIII}},
  pages     = {173-198}}

@book         {gordon79,
  author    = {M. J. Gordon, A. J. Milner, C. P. Wadsworth},
  title     = {Edinburgh {LCF}, A mechanised logic of computation},
  publisher = {Springer-Verlag},
  year      = {1979},
  volume    = {78},
  series    = {Lecture Notes in Computer Science}}

@article      {grue92,
  author    = {K. Grue},
  title     = {Map Theory},
  journal   = TCS,
  year      = {1992},
  volume    = {102},
  number    = {1},
  pages     = {1--133},
  month     = {jul}}

@book         {MathComp,
  author    = {Klaus Grue},
  year      = {2001},
  title     = {Mathematics and Computation},
  publisher = {DIKU},
  address   = {Universitetsparken 1, DK-2100 Copenhagen},
  volume    = {1--3},
  edition   = {7},
  keywords  = {Logic}}
 
@misc         {MathML,
  author    = {Robert Miner and Jeff Schaeffer},
  title     = {A Gentle Introduction to {MathML}},
  TYPE      = {Tutorial},        
  note      = {\url
               {http://www.dessci.com/en/support/tutorials/mathml/default.htm}},
  year      = {2001}}

@techreport{grue02b,
  author    = {K. Grue},
  year      = {2002},
  title     = {Map Theory with Classical Maps},
  institution
            = {DIKU},
  note      = {\url{http://www.diku.dk/publikationer/tekniske.rapporter/2002/}},
  number    = {02/21}}

@inproceedings{grue04,
  author    = {K. Grue},
  title     = {Logiweb},
  editor    = {Fairouz Kamareddine},
  booktitle = {Mathematical Knowledge Management Symposium 2003},
  publisher = {Elsevier},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {93},
  year      = {2004},
  pages     = {70--101}}

@InProceedings{grue05,
  author     = {K. Grue},
  year       = {2005},
  title      = {The implementation of Logiweb},
  booktitle  = {Empirically Successful Classical Automated Reasoning
               (ESCAR)},
  editor     = {Bernd Fischer and Stephan Schulz and Geoff Sutcliffe},
  keywords   = {Automated Reasoning, Electronic Publishing}}

@techreport{base,
  author    = {K. Grue},
  year      = {2006},
  title     = {A Logiweb base page},
  institution={Logiweb},
  note      = {{\small \url{\lgwBaseUrl}}}}

@techreport{appendix,
  author    = {K. Grue},
  year      = {2006},
  title     = {Logiweb sequent calculus, appendix},
  institution={Logiweb},
  note      = {{\small \url{\lgwCheckUrl body/tex/appendix.pdf}}}}

@misc         {kohlhase03,
  author    = {Michael Kohlhase},
  title     = {{OMDoc}: An Open Markup Format for Mathematical Documents 
               (Version 1.1)},
  type      = {Open Specification},
  note      = {\url{http://www.mathweb.org/omdoc.ps}},
  year      = {2003}}

@article      {mccarthy60,
   author   = {J. McCarthy},
   title    = {Recursive functions of symbolic expressions and their 
               computation by machine},
   journal  = {Communications of the ACM},
   year     = {1960},
   pages    = {184--195}}

@book         {mendelson,
  author    = {E. Mendelson},
  title     = {Introduction to Mathematical Logic},
  publisher = {Wadsworth and Brooks},
  year      = {1987},
  edition   = {3.}}

@manual       {matuszewski93,
  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}}

@techreport   {paulson98a,
  author    = {Lawrence C. Paulson},
  title     = {Introduction to {Isabelle}},
  institution
            = {University of Cambridge, Computer Laboratory},
  year      = {1998}}

@techreport   {paulson98b,
  author    = {Lawrence C. Paulson},
  title     = {The {Isabelle} Reference Manual},
  institution
            = {University of Cambridge, Computer Laboratory},
  year      = {1998}}

@phdthesis    {skalberg02,
  author    = {Sebastian C. Skalberg},
  title     = {An Interactive Proof System for Map Theory},
  school    = {University of Copenhagen},
  year      = {2002},
  month     = {oct},
  note      = {\url{http://www.mangust.dk/skalberg/phd/}},
  postscript= {\url{http://www.mangust.dk/skalberg/phd/skalberg-phd.ps}}}

@Book         {steele,
  author    = {Guy L. Steele},
  title     = {Common Lisp---The Language},
  publisher = {Digital Press},
  year      = {1990},
  edition   = {2.}}

@book         {TeXbook,
  author    = {D. Knuth},
  title     = {The TeXbook},
  publisher = {Addison Wesley},
  year      = {1983}}

@inproceedings{trybulec85a,
  author    = {Andrzej Trybulec and Howard Blair},
  title     = {Computer Assisted Reasoning with {MIZAR}},
  pages     = {26--28},
  booktitle = {Proceedings of the 9th International Joint Conference on
               Artificial Intelligence},
  editor    = {Aravind Joshi},
  month     = {aug},
  year      = {1985},
  address   = {Los Angeles, CA},
  publisher = {Morgan Kaufmann},
  note      = {\url{http://www.mizar.org/}}}

@book         {vallee03,
  author    = {Thierry Vall\'{e}e},
  title     = {``{Map Theory}'' et Antifondation},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {79},
  publisher = {Elsevier},
  year      = {2003},
  pages     = {1-258}}