@string{CUCL="Comp. Lab., Univ. Camb."}
@string{CUP="Cambridge University Press"}
@string{Springer="Springer-Verlag"}
@string{TUM="TU Munich"}

@article{church40,
  author = "Alonzo Church",
  title  = "A Formulation of the Simple Theory of Types",
  journal = "Journal of Symbolic Logic",
  year  = 1940,
  volume = 5,
  pages  = "56-68"}

@Book{Concrete-Math,
  author =   {R. L. Graham and D. E. Knuth and O. Patashnik},
  title =   {Concrete Mathematics},
  publisher =   {Addison-Wesley},
  year =   1989
}

@InProceedings{Naraschewski-Wenzel:1998:HOOL,
  author = {Wolfgang Naraschewski and Markus Wenzel},
  title  = {Object-Oriented Verification based on Record Subtyping in
                  {H}igher-{O}rder {L}ogic},
  crossref      = {tphols98}}

@Article{Nipkow:1998:Winskel,
  author =   {Tobias Nipkow},
  title =   {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
  journal =   {Formal Aspects of Computing},
  year =   1998,
  volume =  10,
  pages =  {171--186}
}

@InProceedings{Wenzel:1999:TPHOL,
  author =   {Markus Wenzel},
  title =   {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
  crossref =     {tphols99}}

@Book{Winskel:1993,
  author =   {G. Winskel},
  title =   {The Formal Semantics of Programming Languages},
  publisher =   {MIT Press},
  year =   1993
}

@Book{davey-priestley,
  author = {B. A. Davey and H. A. Priestley},
  title  = {Introduction to Lattices and Order},
  publisher = CUP,
  year  = 1990}

@TechReport{Gordon:1985:HOL,
  author =       {M. J. C. Gordon},
  title =        {{HOL}: A machine oriented formulation of higher order logic},
  institution =  {University of Cambridge Computer Laboratory},
  year =         1985,
  number =       68
}

@manual{isabelle-HOL,
  author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title  = {{Isabelle}'s Logics: {HOL}},
  institution = {Institut f\"ur Informatik, Technische Universi\"at
                  M\"unchen and Computer Laboratory, University of Cambridge}}

@manual{isabelle-intro,
  author = {Lawrence C. Paulson},
  title  = {Introduction to {Isabelle}},
  institution = CUCL}

@manual{isabelle-isar-ref,
  author = {Markus Wenzel},
  title  = {The {Isabelle/Isar} Reference Manual},
  institution = TUM}

@manual{isabelle-ref,
  author = {Lawrence C. Paulson},
  title  = {The {Isabelle} Reference Manual},
  institution = CUCL}

@Book{paulson-isa-book,
  author = {Lawrence C. Paulson},
  title  = {Isabelle: A Generic Theorem Prover},
  publisher = {Springer},
  year  = 1994,
  note  = {LNCS 828}}

@TechReport{paulson-mutilated-board,
  author =   {Lawrence C. Paulson},
  title =   {A Simple Formalization and Proof for the Mutilated Chess Board},
  institution =  CUCL,
  year =   1996,
  number =  394,
  note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}
}

@Proceedings{tphols98,
  title  = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
  booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
  editor = {Jim Grundy and Malcom Newey},
  series = {LNCS},
  volume        = 1479,
  year  = 1998}

@Proceedings{tphols99,
  title  = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
                  Paulin, C. and Thery, L.},
  series = {LNCS 1690},
  year  = 1999}