# HG changeset patch
# User nipkow
# Date 925890288 -7200
# Node ID 41b44b20a1b430e8de85f4e11731da6952b5484c
# Parent  6e6ca099f68f30b0f03fae744d9282afc5ae46fc
Bibtex database for documentation.

diff -r 6e6ca099f68f -r 41b44b20a1b4 doc-src/isabelle.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/isabelle.bib	Wed May 05 09:44:48 1999 +0200
@@ -0,0 +1,58 @@
+@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}