Bibtex database for documentation.
@string{AP="Academic Press"}
@string{CUP="Cambridge University Press"}
@string{FAC="Formal Aspects of Computing"}
@string{JSL="J. Symbolic Logic"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
@string{MIT="MIT Press"}
@string{Springer="Springer-Verlag"}
@book{andrews86,author="Peter Andrews",
title="An Introduction to Mathematical Logic and Type Theory: to Truth
through Proof",publisher=AP,
series="Computer Science and Applied Mathematics",year=1986}
@book{mgordon-hol,editor="M.J.C. Gordon and T.F. Melham",
title=
"Introduction to {HOL}: a theorem-proving environment for higher order logic",
publisher=CUP,year=1993}
@article{church40,author="Alonzo Church",
title="A Formulation of the Simple Theory of Types",
journal=JSL,year=1940,volume=5,pages="56--68"}
@article{milner78,author="Robin Milner",
title="A Theory of Type Polymorphism in Programming",
journal="J. Comp.\ Sys.\ Sci.",year=1978,volume=17,pages="348--375"}
@InProceedings{NaraschewskiW-TPHOLs98,
author={Wolfgang Naraschewski and Markus Wenzel},
title=
{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs'98)},
publisher=Springer,volume=1479,series=LNCS,year=1998}
@inproceedings{nipkow-W,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
booktitle={Types for Proofs and Programs: Intl. Workshop TYPES '96},
editor={E. Gim\'enez and C. Paulin-Mohring},
publisher=Springer,series=LNCS,volume=1512,pages={317--332},year=1998}
@inproceedings{Nipkow-CR,author={Tobias Nipkow},
title={More {Church-Rosser} Proofs (in {Isabelle/HOL})},
booktitle={Automated Deduction --- CADE-13},
editor={M. McRobbie and J.K. Slaney},
publisher=Springer,series=LNCS,volume=1104,pages={733--747},year=1996}
@article{nipkow-IMP,author={Tobias Nipkow},
title={Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
journal=FAC,volume=10,pages={171--186},year=1998}
@inproceedings{slind-tfl,author={Konrad Slind},
title={Function Definition in Higher Order Logic},
booktitle={Theorem Proving in Higher Order Logics},
editor={J. von Wright and J. Grundy and J. Harrison},
publisher=Springer,series=LNCS,volume=1125,pages={381--397},year=1996}
@book{winskel93,author={Glynn Winskel},
title={The Formal Semantics of Programming Languages},publisher=MIT,year=1993}