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