@string{CUCL="Comp. Lab., Univ. Camb."}
@string{CUP="Cambridge University Press"}
@string{Springer="Springer-Verlag"}
@string{TUM="TU Munich"}
@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}
@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}
@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.ftp.cl.cam.ac.uk/ftp/papers/reports/}}
}
@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}