doc-src/Locales/Locales/document/root.bib
author ballarin
Fri, 16 Apr 2004 11:35:44 +0200
changeset 14586 7b8d56b4ac60
child 16168 adb83939177f
permissions -rw-r--r--
Added Locales Tutorial.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     1
@phdthesis{Bailey1998,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     2
  author = "Anthony Bailey",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     3
  title = "The machine-checked literate formalisation of algebra in type theory",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     4
  school = "University of Manchester",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
  month = jan,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
  year = 1998,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     8
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     9
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
@phdthesis{Kammuller1999a,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    11
  author = "Florian Kamm{\"u}ller",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    12
  title = "Modular Reasoning in {Isabelle}",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    13
  school = "University of Cambridge, Computer Laboratory",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
  note = "Available as Technical Report No. 470.",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
  month = aug,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    16
  year = 1999,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    17
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    18
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    19
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    20
% TYPES 98
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
@inproceedings{Kammuller1999b,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
  author = "Florian Kamm{\"u}ller",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
  title = "Modular Structures as Dependent Types in {Isabelle}",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
  pages = "121--132",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
  crossref = "AltenkirchEtAl1999",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    27
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    28
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    29
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
@proceedings{AltenkirchEtAl1999,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
  editor = "Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
  title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    33
  booktitle = "TYPES '98",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
  publisher = "Springer",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    35
  series = "LNCS",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    36
  number = 1657,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    37
  year = 1999
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    38
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    39
% CADE-17
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    40
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    41
@inproceedings{Kammuller2000,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    42
  author = "Florian Kamm{\"u}ller",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
  title = "Modular Reasoning in {Isabelle}",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
  pages = "99--114",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    45
  crossref = "McAllester2000",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    46
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    47
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    49
@proceedings{McAllester2000,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    50
  editor = "David McAllester",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    51
  title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    52
  booktitle = "CADE 17",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    53
  publisher = "Springer",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    54
  series = "LNCS",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    55
  number = 1831,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    56
  year = 2000
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    57
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    58
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    59
@book{NipkowEtAl2002,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    60
  author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    61
  title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    62
  publisher = "Springer",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    63
  series = "LNCS",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    64
  number = 2283,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    65
  year = 2002,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    66
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    67
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    68
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    69
% TYPES 2002
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    70
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    71
@inproceedings{Nipkow2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    72
  author = "Tobias Nipkow",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    73
  title = "Structured Proofs in {Isar/HOL}",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    74
  pages = "259--278",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    75
  crossref = "GeuversWiedijk2003"
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    76
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    77
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    78
@proceedings{GeuversWiedijk2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    79
  editor = "H. Geuvers and F. Wiedijk",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    80
  title = "Types for Proofs and Programs (TYPES 2002)",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    81
  booktitle = "TYPES 2002",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    82
  publisher = "Springer",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    83
  series = "LNCS",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    84
  number = 2646,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    85
  year = 2003
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    86
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    87
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    88
@phdthesis{Wenzel2002a,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    89
  author = "Markus Wenzel",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    90
  title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    91
  school = "Technische Universit{\"a}t M{\"u}nchen",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    92
  note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    93
  year = 2002
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    94
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    95
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    96
@unpublished{Wenzel2002b,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    97
  author = "Markus Wenzel",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    98
  title = "Using locales in {Isabelle/Isar}",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    99
  note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy.  Distribution of Isabelle available at http://isabelle.in.tum.de",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   100
  year = 2002
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   101
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   102
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   103
@unpublished{Wenzel2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   104
  author = "Markus Wenzel",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   105
  title = "The {Isabelle/Isar} Reference Manual",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   106
  note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   107
  year = 2003
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   108
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   109
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   110
% TPHOLs 2003
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   111
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   112
@inproceedings{Chrzaszcz2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   113
  author = "Jacek Chrzaszcz",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   114
  title = "Implementing Modules in the {Coq} System",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   115
  pages = "270--286",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   116
  crossref = "BasinWolff2003",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   117
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   118
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   119
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   120
@proceedings{BasinWolff2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   121
  editor = "David Basin and Burkhart Wolff",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   122
  title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   123
  booktitle = "TPHOLs 2003",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   124
  publisher = "Springer",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   125
  series = "LNCS",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   126
  number = 2758,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   127
  year = 2003
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   128
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   129
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   130
@PhdThesis{Klein2003,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   131
  author = "Gerwin Klein",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   132
  title = "Verified Java Bytecode Verification",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   133
  school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   134
  year = 2003
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   135
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   136
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   137
% TACAS 2000
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   138
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   139
@inproceedings{Aspinall2000,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   140
  author = "David Aspinall",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   141
  title = "Proof General: A Generic Tool for Proof Development",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   142
  pages = "38--42",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   143
  crossref = "GrafSchwartzbach2000"
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   144
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   145
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   146
@proceedings{GrafSchwartzbach2000,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   147
  editor    = {Susanne Graf and Michael I. Schwartzbach},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   148
  title     = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   149
  booktitle     = "TACAS 2000",
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   150
  publisher = {Springer},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   151
  series    = {LNCS},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   152
  number    = {1785},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   153
  year      = {2000},
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   154
}