@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

}

@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},

title={Compiling Exceptions Correctly},

booktitle={Proc.\ Conf.\ Mathematics of Program Construction},

year=2004,note={To appear}}

@InProceedings{Kamm-et-al:1999,

  author =       {Florian Kamm{\"u}ller and Markus Wenzel and

                  Lawrence C. Paulson},

  title =        {Locales: A Sectioning Concept for {Isabelle}},

  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},

  volume        = 1690,

  year          = 1999}

@InProceedings{Naraschewski-Wenzel:1998,

  author        = {Wolfgang Naraschewski and Markus Wenzel},

  title         = {Object-Oriented Verification based on Record Subtyping in

                  {H}igher-{O}rder {L}ogic},

  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

  editor        = {Jim Grundy and Malcom Newey},

  series        = {LNCS},

  volume        = 1479,

  year          = 1998}

@Manual{Nipkow-et-al:2001:HOL,

  author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

  title         = {{Isabelle}'s Logics: {HOL}},

  institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t

                  M{\"u}nchen and Computer Laboratory, University of Cambridge},

  year          = 2001,

  note          = {Part of the Isabelle distribution,

                   \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}

}

@Article{Paulson:1989,

  author =       {L. C. Paulson},

  title =        {The foundation of a generic Theorem Prover},

  journal =      {Journal of Automated Reasoning},

  year =         1989,

  volume =       5,

  number =       3,

  pages =        {363--397}

}

@Book{Paulson:1994:Isabelle,

 author =        {L. C. Paulson and T. Nipkow},

  title =        {{Isabelle}: A Generic Theorem Prover},

  year =         1994,

  series =       {LNCS},

  volume =       {828},

  publisher =    {Springer}

}

@InProceedings{Wenzel:1999,

  author =       {Markus Wenzel},

  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},

  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},

  volume        = 1690,

  year          = 1999}

@Unpublished{Wenzel:2001:Isar-examples,

  author =       {Markus Wenzel},

  title =        {Miscellaneous {I}sabelle/{I}sar examples for

                  Higher-Order Logic},

  year =         2001,

  note =         {Part of the Isabelle distribution,

                  \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/document.pdf}}

}

@PhdThesis{Wenzel:2001:Thesis,

  author = 	 {Markus Wenzel},

  title = 	 {Isabelle/Isar --- a versatile environment for human-readable

                  formal proof documents},

  school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},

  year = 	 2001,

  month =	 {September},

  note =	 {Submitted}

}

@Manual{Wenzel:2001:isar-ref,

  author        = {Markus Wenzel},

  title         = {The {Isabelle/Isar} Reference Manual},

  year          = 2001,

  institution   = {TU M{\"u}nchen},

  note          = {Part of the Isabelle distribution,

                   \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}

}

@Book{isabelle-hol-book,

  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},

  publisher	= {Springer},

  year		= 2002,

  note		= {LNCS 2283}}

@Misc{McMillan-LectureNotes,

  author =	 {Ken McMillan},

  title =	 {Lecture notes on verification of digital and hybrid systems},

  note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}

}

@PhdThesis{McMillan-PhDThesis,

  author = 	 {Ken McMillan},

  title = 	 {Symbolic Model Checking: an approach to the state explosion problem},

  school = 	 {Carnegie Mellon University},

  year = 	 1992

}