doc-src/Locales/Locales/document/root.bib
author ballarin
Tue, 03 Jun 2008 12:34:22 +0200
changeset 27063 d1d35284542f
parent 16168 adb83939177f
child 32981 0114e04a0d64
permissions -rw-r--r--
New version covering interpretation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     1
@unpublished{IsarRef,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     2
  author = "Markus Wenzel",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     3
  title = "The {Isabelle/Isar} Reference Manual",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     4
  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     7
@book {Jacobson1985,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     8
  author = "Nathan Jacobson",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     9
  title = "Basic Algebra",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    10
  volume = "I",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    11
  publisher = "Freeman",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    12
  edition = "2nd",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    13
  year = 1985,
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    16
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    17
% TYPES 2006
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    18
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    19
@inproceedings{HaftmannWenzel2007,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    20
  author = "Florian Haftmann and Makarius Wenzel",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    21
  title = "Constructive Type Classes in {Isabelle}",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    22
  pages = "160--174",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    23
  crossref = "AltenkirchMcBride2007",
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    27
@proceedings{AltenkirchMcBride2007,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    28
  editor = "Thorsten Altenkirch and Connor McBride",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    29
  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    30
  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
  publisher = "Springer",
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    32
  series = "LNCS 4502",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    33
  year = 2007
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    35
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    36
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    37
@techreport{Ballarin2006a,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    38
  author = "Clemens Ballarin",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    39
  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    40
  institution = "Technische Universit{\"a}t M{\"u}nchen",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    41
  number = "TUM-I0607",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    42
  year = 2006
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    45
% MKM 2006
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    46
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    47
@inproceedings{Ballarin2006b,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    48
  author = "Clemens Ballarin",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    49
  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    50
  pages = "31--43",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    51
  crossref = "BorweinFarmer2006"
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    52
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    53
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    54
@proceedings{BorweinFarmer2006,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    55
  editor = "Jonathan M. Borwein and William M. Farmer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    56
  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    57
  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    58
  series = "LNCS 4108",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    59
  publisher = "Springer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    60
  year = 2006,
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    61
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    62
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    63
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    64
% TPHOLs 1999
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    65
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    66
@inproceedings{KammullerEtAl1999,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    67
  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    68
  title = "Locales: A Sectioning Concept for {Isabelle}",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    69
  pages = "149--165",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    70
  crossref = "BertotEtAl1999",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    71
  available = { CB }
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    72
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    73
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    74
@book{BertotEtAl1999,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    75
  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    76
  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    77
  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    78
  publisher = "Springer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    79
  series = "LNCS 1690",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    80
  year = 1999
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 14586
diff changeset
    81
}