src/HOL/Isar_examples/document/root.bib
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10148 739327964a5c
child 14378 69c4d5997669
permissions -rw-r--r--
improved theory reference in comment
wenzelm@7816
     1
wenzelm@7816
     2
@string{CUCL="Comp. Lab., Univ. Camb."}
wenzelm@7816
     3
@string{CUP="Cambridge University Press"}
wenzelm@7816
     4
@string{Springer="Springer-Verlag"}
wenzelm@7816
     5
@string{TUM="TU Munich"}
wenzelm@7816
     6
wenzelm@8051
     7
@Book{Concrete-Math,
wenzelm@8051
     8
  author = 	 {R. L. Graham and D. E. Knuth and O. Patashnik},
wenzelm@8051
     9
  title = 	 {Concrete Mathematics},
wenzelm@8051
    10
  publisher = 	 {Addison-Wesley},
wenzelm@8051
    11
  year = 	 1989
wenzelm@8051
    12
}
wenzelm@8051
    13
wenzelm@10148
    14
@InProceedings{Naraschewski-Wenzel:1998:HOOL,
wenzelm@10148
    15
  author	= {Wolfgang Naraschewski and Markus Wenzel},
wenzelm@10148
    16
  title		= {Object-Oriented Verification based on Record Subtyping in
wenzelm@10148
    17
                  {H}igher-{O}rder {L}ogic},
wenzelm@10148
    18
  crossref      = {tphols98}}
wenzelm@10148
    19
wenzelm@10148
    20
@Article{Nipkow:1998:Winskel,
wenzelm@10148
    21
  author = 	 {Tobias Nipkow},
wenzelm@10148
    22
  title = 	 {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
wenzelm@10148
    23
  journal = 	 {Formal Aspects of Computing},
wenzelm@10148
    24
  year = 	 1998,
wenzelm@10148
    25
  volume =	 10,
wenzelm@10148
    26
  pages =	 {171--186}
wenzelm@10148
    27
}
wenzelm@10148
    28
wenzelm@7968
    29
@InProceedings{Wenzel:1999:TPHOL,
wenzelm@7968
    30
  author = 	 {Markus Wenzel},
wenzelm@7968
    31
  title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
wenzelm@7968
    32
  crossref =     {tphols99}}
wenzelm@7968
    33
wenzelm@10148
    34
@Book{Winskel:1993,
wenzelm@10148
    35
  author = 	 {G. Winskel},
wenzelm@10148
    36
  title = 	 {The Formal Semantics of Programming Languages},
wenzelm@10148
    37
  publisher = 	 {MIT Press},
wenzelm@10148
    38
  year = 	 1993
wenzelm@10148
    39
}
wenzelm@10148
    40
wenzelm@7816
    41
@Book{davey-priestley,
wenzelm@7816
    42
  author	= {B. A. Davey and H. A. Priestley},
wenzelm@7816
    43
  title		= {Introduction to Lattices and Order},
wenzelm@7816
    44
  publisher	= CUP,
wenzelm@7816
    45
  year		= 1990}
wenzelm@7816
    46
wenzelm@7816
    47
@manual{isabelle-HOL,
wenzelm@7816
    48
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
wenzelm@7816
    49
  title		= {{Isabelle}'s Logics: {HOL}},
wenzelm@7816
    50
  institution	= {Institut f\"ur Informatik, Technische Universi\"at
wenzelm@7816
    51
                  M\"unchen and Computer Laboratory, University of Cambridge}}
wenzelm@7816
    52
wenzelm@7816
    53
@manual{isabelle-intro,
wenzelm@7816
    54
  author	= {Lawrence C. Paulson},
wenzelm@7816
    55
  title		= {Introduction to {Isabelle}},
wenzelm@7816
    56
  institution	= CUCL}
wenzelm@7816
    57
wenzelm@7816
    58
@manual{isabelle-isar-ref,
wenzelm@7816
    59
  author	= {Markus Wenzel},
wenzelm@7968
    60
  title		= {The {Isabelle/Isar} Reference Manual},
wenzelm@7816
    61
  institution	= TUM}
wenzelm@7816
    62
wenzelm@7968
    63
@manual{isabelle-ref,
wenzelm@7968
    64
  author	= {Lawrence C. Paulson},
wenzelm@7968
    65
  title		= {The {Isabelle} Reference Manual},
wenzelm@7968
    66
  institution	= CUCL}
wenzelm@7968
    67
wenzelm@7968
    68
@TechReport{paulson-mutilated-board,
wenzelm@7968
    69
  author = 	 {Lawrence C. Paulson},
wenzelm@7968
    70
  title = 	 {A Simple Formalization and Proof for the Mutilated Chess Board},
wenzelm@7968
    71
  institution =  CUCL,
wenzelm@7968
    72
  year = 	 1996,
wenzelm@7968
    73
  number =	 394,
wenzelm@7977
    74
  note = {\url{http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/}}
wenzelm@7968
    75
}
wenzelm@7816
    76
wenzelm@10148
    77
@Proceedings{tphols98,
wenzelm@10148
    78
  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
wenzelm@10148
    79
  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
wenzelm@10148
    80
  editor	= {Jim Grundy and Malcom Newey},
wenzelm@10148
    81
  series	= {LNCS},
wenzelm@10148
    82
  volume        = 1479,
wenzelm@10148
    83
  year		= 1998}
wenzelm@10148
    84
wenzelm@7816
    85
@Proceedings{tphols99,
wenzelm@7816
    86
  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm@7816
    87
  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm@7816
    88
  editor	= {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
wenzelm@7816
    89
                  Paulin, C. and Thery, L.},
wenzelm@7816
    90
  series	= {LNCS 1690},
wenzelm@7816
    91
  year		= 1999}