src/HOL/ex/document/root.bib
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 15871 e524119dbf19
child 33026 8f35633c4922
permissions -rw-r--r--
added lemmas
bauerg@15871
     1
bauerg@15871
     2
wenzelm@12360
     3
wenzelm@12360
     4
@TechReport{Gordon:1985:HOL,
wenzelm@12360
     5
  author =       {M. J. C. Gordon},
wenzelm@12360
     6
  title =        {{HOL}: A machine oriented formulation of higher order logic},
wenzelm@12360
     7
  institution =  {University of Cambridge Computer Laboratory},
wenzelm@12360
     8
  year =         1985,
wenzelm@12360
     9
  number =       68
wenzelm@12360
    10
}
wenzelm@12101
    11
nipkow@14569
    12
@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
nipkow@14569
    13
title={Compiling Exceptions Correctly},
nipkow@14569
    14
booktitle={Proc.\ Conf.\ Mathematics of Program Construction},
nipkow@14569
    15
year=2004,note={To appear}}
nipkow@14569
    16
wenzelm@12101
    17
@InProceedings{Kamm-et-al:1999,
wenzelm@12101
    18
  author =       {Florian Kamm{\"u}ller and Markus Wenzel and
wenzelm@12101
    19
                  Lawrence C. Paulson},
wenzelm@12101
    20
  title =        {Locales: A Sectioning Concept for {Isabelle}},
wenzelm@12101
    21
  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm@12101
    22
  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
wenzelm@12101
    23
                  Paulin, C. and Thery, L.},
wenzelm@12101
    24
  series        = {LNCS},
wenzelm@12101
    25
  volume        = 1690,
wenzelm@12101
    26
  year          = 1999}
wenzelm@12101
    27
wenzelm@12101
    28
@InProceedings{Naraschewski-Wenzel:1998,
wenzelm@12101
    29
  author        = {Wolfgang Naraschewski and Markus Wenzel},
wenzelm@12101
    30
  title         = {Object-Oriented Verification based on Record Subtyping in
wenzelm@12101
    31
                  {H}igher-{O}rder {L}ogic},
wenzelm@12101
    32
  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
wenzelm@12101
    33
  editor        = {Jim Grundy and Malcom Newey},
wenzelm@12101
    34
  series        = {LNCS},
wenzelm@12101
    35
  volume        = 1479,
wenzelm@12101
    36
  year          = 1998}
wenzelm@12101
    37
wenzelm@12101
    38
@Manual{Nipkow-et-al:2001:HOL,
wenzelm@12101
    39
  author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
wenzelm@12101
    40
  title         = {{Isabelle}'s Logics: {HOL}},
wenzelm@12101
    41
  institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
wenzelm@12101
    42
                  M{\"u}nchen and Computer Laboratory, University of Cambridge},
wenzelm@12101
    43
  year          = 2001,
wenzelm@12101
    44
  note          = {Part of the Isabelle distribution,
wenzelm@12101
    45
                   \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
wenzelm@12101
    46
}
wenzelm@12101
    47
wenzelm@12900
    48
@Article{Paulson:1989,
wenzelm@12900
    49
  author =       {L. C. Paulson},
wenzelm@12900
    50
  title =        {The foundation of a generic Theorem Prover},
wenzelm@12900
    51
  journal =      {Journal of Automated Reasoning},
wenzelm@12900
    52
  year =         1989,
wenzelm@12900
    53
  volume =       5,
wenzelm@12900
    54
  number =       3,
wenzelm@12900
    55
  pages =        {363--397}
wenzelm@12900
    56
}
wenzelm@12900
    57
wenzelm@13446
    58
@Book{Paulson:1994:Isabelle,
wenzelm@13446
    59
 author =        {L. C. Paulson and T. Nipkow},
wenzelm@13446
    60
  title =        {{Isabelle}: A Generic Theorem Prover},
wenzelm@13446
    61
  year =         1994,
wenzelm@13446
    62
  series =       {LNCS},
wenzelm@13446
    63
  volume =       {828},
wenzelm@13446
    64
  publisher =    {Springer}
wenzelm@13446
    65
}
wenzelm@13446
    66
wenzelm@12101
    67
@InProceedings{Wenzel:1999,
wenzelm@12101
    68
  author =       {Markus Wenzel},
wenzelm@12101
    69
  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
wenzelm@12101
    70
  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
wenzelm@12101
    71
  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
wenzelm@12101
    72
                  Paulin, C. and Thery, L.},
wenzelm@12101
    73
  series        = {LNCS},
wenzelm@12101
    74
  volume        = 1690,
wenzelm@12101
    75
  year          = 1999}
wenzelm@12101
    76
wenzelm@12508
    77
@Unpublished{Wenzel:2001:Isar-examples,
wenzelm@12508
    78
  author =       {Markus Wenzel},
wenzelm@12508
    79
  title =        {Miscellaneous {I}sabelle/{I}sar examples for
wenzelm@12508
    80
                  Higher-Order Logic},
wenzelm@12508
    81
  year =         2001,
wenzelm@12508
    82
  note =         {Part of the Isabelle distribution,
wenzelm@12508
    83
                  \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/document.pdf}}
wenzelm@12508
    84
}
wenzelm@13446
    85
wenzelm@12101
    86
@PhdThesis{Wenzel:2001:Thesis,
wenzelm@12101
    87
  author = 	 {Markus Wenzel},
wenzelm@12101
    88
  title = 	 {Isabelle/Isar --- a versatile environment for human-readable
wenzelm@12101
    89
                  formal proof documents},
wenzelm@12101
    90
  school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
wenzelm@12101
    91
  year = 	 2001,
wenzelm@12101
    92
  month =	 {September},
wenzelm@12101
    93
  note =	 {Submitted}
wenzelm@12101
    94
}
wenzelm@12101
    95
@Manual{Wenzel:2001:isar-ref,
wenzelm@12101
    96
  author        = {Markus Wenzel},
wenzelm@12101
    97
  title         = {The {Isabelle/Isar} Reference Manual},
wenzelm@12101
    98
  year          = 2001,
wenzelm@12101
    99
  institution   = {TU M{\"u}nchen},
wenzelm@12101
   100
  note          = {Part of the Isabelle distribution,
wenzelm@12101
   101
                   \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
wenzelm@12101
   102
}
wenzelm@13446
   103
wenzelm@13446
   104
@Book{isabelle-hol-book,
wenzelm@13446
   105
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
wenzelm@13446
   106
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
wenzelm@13446
   107
  publisher	= {Springer},
wenzelm@13446
   108
  year		= 2002,
wenzelm@13446
   109
  note		= {LNCS 2283}}
bauerg@15871
   110
bauerg@15871
   111
@Misc{McMillan-LectureNotes,
bauerg@15871
   112
  author =	 {Ken McMillan},
bauerg@15871
   113
  title =	 {Lecture notes on verification of digital and hybrid systems},
bauerg@15871
   114
  note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
bauerg@15871
   115
}
bauerg@15871
   116
bauerg@15871
   117
@PhdThesis{McMillan-PhDThesis,
bauerg@15871
   118
  author = 	 {Ken McMillan},
bauerg@15871
   119
  title = 	 {Symbolic Model Checking: an approach to the state explosion problem},
bauerg@15871
   120
  school = 	 {Carnegie Mellon University},
bauerg@15871
   121
  year = 	 1992
bauerg@15871
   122
}