src/Doc/Locales/document/root.bib
author wenzelm
Wed Jul 18 16:44:01 2018 +0200 (10 months ago)
changeset 68649 f849fc1cb65e
parent 48985 5386df44a037
permissions -rw-r--r--
prefer HTTPS;
ballarin@27063
     1
@unpublished{IsarRef,
ballarin@27063
     2
  author = "Markus Wenzel",
ballarin@27063
     3
  title = "The {Isabelle/Isar} Reference Manual",
wenzelm@68649
     4
  note = "Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}."
ballarin@14586
     5
}
ballarin@14586
     6
ballarin@27063
     7
@book {Jacobson1985,
ballarin@27063
     8
  author = "Nathan Jacobson",
ballarin@27063
     9
  title = "Basic Algebra",
ballarin@27063
    10
  volume = "I",
ballarin@27063
    11
  publisher = "Freeman",
ballarin@27063
    12
  edition = "2nd",
ballarin@27063
    13
  year = 1985,
ballarin@14586
    14
  available = { CB }
ballarin@14586
    15
}
ballarin@14586
    16
ballarin@27063
    17
% TYPES 2006
ballarin@14586
    18
ballarin@27063
    19
@inproceedings{HaftmannWenzel2007,
ballarin@27063
    20
  author = "Florian Haftmann and Makarius Wenzel",
ballarin@27063
    21
  title = "Constructive Type Classes in {Isabelle}",
ballarin@27063
    22
  pages = "160--174",
ballarin@27063
    23
  crossref = "AltenkirchMcBride2007",
ballarin@14586
    24
  available = { CB }
ballarin@14586
    25
}
ballarin@14586
    26
ballarin@27063
    27
@proceedings{AltenkirchMcBride2007,
ballarin@27063
    28
  editor = "Thorsten Altenkirch and Connor McBride",
ballarin@27063
    29
  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
ballarin@27063
    30
  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
ballarin@14586
    31
  publisher = "Springer",
ballarin@27063
    32
  series = "LNCS 4502",
ballarin@27063
    33
  year = 2007
ballarin@14586
    34
}
ballarin@14586
    35
ballarin@14586
    36
ballarin@27063
    37
@techreport{Ballarin2006a,
ballarin@27063
    38
  author = "Clemens Ballarin",
ballarin@27063
    39
  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
ballarin@27063
    40
  institution = "Technische Universit{\"a}t M{\"u}nchen",
ballarin@27063
    41
  number = "TUM-I0607",
ballarin@27063
    42
  year = 2006
ballarin@14586
    43
}
ballarin@14586
    44
ballarin@32983
    45
% TYPES 2003
ballarin@32983
    46
ballarin@32983
    47
@inproceedings{Ballarin2004a,
ballarin@32983
    48
  author = "Clemens Ballarin",
ballarin@32983
    49
  title = "Locales and Locale Expressions in {Isabelle/Isar}",
ballarin@32983
    50
  pages = "34--50",
ballarin@32983
    51
  crossref = "BerardiEtAl2004"
ballarin@32983
    52
}
ballarin@32983
    53
ballarin@32983
    54
@proceedings{BerardiEtAl2004,
ballarin@32983
    55
  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
ballarin@32983
    56
  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
ballarin@32983
    57
  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
ballarin@32983
    58
  publisher = "Springer",
ballarin@32983
    59
  series = "LNCS 3085",
ballarin@32983
    60
  year = 2004
ballarin@32983
    61
}
ballarin@32983
    62
ballarin@32981
    63
% TYPES 2008
ballarin@32981
    64
ballarin@32981
    65
@inproceedings{HaftmannWenzel2009,
ballarin@32981
    66
  author = "Florian Haftmann and Makarius Wenzel",
ballarin@32981
    67
  title = "Local theory specifications in {Isabelle}/{Isar}",
ballarin@32981
    68
  pages = "153--168",
ballarin@32981
    69
  crossref = "BerardiEtAl2009"
ballarin@32981
    70
}
ballarin@32981
    71
ballarin@32981
    72
@proceedings{BerardiEtAl2009,
ballarin@32981
    73
  editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
ballarin@32981
    74
  title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
ballarin@32981
    75
  booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
ballarin@32981
    76
  series = "LNCS 5497",
ballarin@32981
    77
  publisher = "Springer",
ballarin@32981
    78
  year = 2009
ballarin@32981
    79
}
ballarin@32981
    80
ballarin@27063
    81
% MKM 2006
ballarin@27063
    82
ballarin@27063
    83
@inproceedings{Ballarin2006b,
ballarin@27063
    84
  author = "Clemens Ballarin",
ballarin@27063
    85
  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
ballarin@27063
    86
  pages = "31--43",
ballarin@27063
    87
  crossref = "BorweinFarmer2006"
ballarin@14586
    88
}
ballarin@14586
    89
ballarin@27063
    90
@proceedings{BorweinFarmer2006,
ballarin@27063
    91
  editor = "Jonathan M. Borwein and William M. Farmer",
ballarin@27063
    92
  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
ballarin@27063
    93
  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
ballarin@27063
    94
  series = "LNCS 4108",
ballarin@27063
    95
  publisher = "Springer",
ballarin@27063
    96
  year = 2006,
ballarin@14586
    97
  available = { CB }
ballarin@14586
    98
}
ballarin@14586
    99
ballarin@27063
   100
% TPHOLs 1999
ballarin@14586
   101
ballarin@27063
   102
@inproceedings{KammullerEtAl1999,
ballarin@27063
   103
  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
ballarin@27063
   104
  title = "Locales: A Sectioning Concept for {Isabelle}",
ballarin@27063
   105
  pages = "149--165",
ballarin@27063
   106
  crossref = "BertotEtAl1999",
ballarin@27063
   107
  available = { CB }
ballarin@14586
   108
}
ballarin@14586
   109
ballarin@27063
   110
@book{BertotEtAl1999,
ballarin@27063
   111
  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
ballarin@27063
   112
  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
ballarin@27063
   113
  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
ballarin@27063
   114
  publisher = "Springer",
ballarin@27063
   115
  series = "LNCS 1690",
ballarin@27063
   116
  year = 1999
ballarin@16168
   117
}