src/Doc/Locales/document/root.bib
changeset 48985 5386df44a037
parent 48943 54da920baf38
child 68649 f849fc1cb65e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Locales/document/root.bib	Tue Aug 28 18:57:32 2012 +0200
     1.3 @@ -0,0 +1,117 @@
     1.4 +@unpublished{IsarRef,
     1.5 +  author = "Markus Wenzel",
     1.6 +  title = "The {Isabelle/Isar} Reference Manual",
     1.7 +  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
     1.8 +}
     1.9 +
    1.10 +@book {Jacobson1985,
    1.11 +  author = "Nathan Jacobson",
    1.12 +  title = "Basic Algebra",
    1.13 +  volume = "I",
    1.14 +  publisher = "Freeman",
    1.15 +  edition = "2nd",
    1.16 +  year = 1985,
    1.17 +  available = { CB }
    1.18 +}
    1.19 +
    1.20 +% TYPES 2006
    1.21 +
    1.22 +@inproceedings{HaftmannWenzel2007,
    1.23 +  author = "Florian Haftmann and Makarius Wenzel",
    1.24 +  title = "Constructive Type Classes in {Isabelle}",
    1.25 +  pages = "160--174",
    1.26 +  crossref = "AltenkirchMcBride2007",
    1.27 +  available = { CB }
    1.28 +}
    1.29 +
    1.30 +@proceedings{AltenkirchMcBride2007,
    1.31 +  editor = "Thorsten Altenkirch and Connor McBride",
    1.32 +  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
    1.33 +  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
    1.34 +  publisher = "Springer",
    1.35 +  series = "LNCS 4502",
    1.36 +  year = 2007
    1.37 +}
    1.38 +
    1.39 +
    1.40 +@techreport{Ballarin2006a,
    1.41 +  author = "Clemens Ballarin",
    1.42 +  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
    1.43 +  institution = "Technische Universit{\"a}t M{\"u}nchen",
    1.44 +  number = "TUM-I0607",
    1.45 +  year = 2006
    1.46 +}
    1.47 +
    1.48 +% TYPES 2003
    1.49 +
    1.50 +@inproceedings{Ballarin2004a,
    1.51 +  author = "Clemens Ballarin",
    1.52 +  title = "Locales and Locale Expressions in {Isabelle/Isar}",
    1.53 +  pages = "34--50",
    1.54 +  crossref = "BerardiEtAl2004"
    1.55 +}
    1.56 +
    1.57 +@proceedings{BerardiEtAl2004,
    1.58 +  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
    1.59 +  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
    1.60 +  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
    1.61 +  publisher = "Springer",
    1.62 +  series = "LNCS 3085",
    1.63 +  year = 2004
    1.64 +}
    1.65 +
    1.66 +% TYPES 2008
    1.67 +
    1.68 +@inproceedings{HaftmannWenzel2009,
    1.69 +  author = "Florian Haftmann and Makarius Wenzel",
    1.70 +  title = "Local theory specifications in {Isabelle}/{Isar}",
    1.71 +  pages = "153--168",
    1.72 +  crossref = "BerardiEtAl2009"
    1.73 +}
    1.74 +
    1.75 +@proceedings{BerardiEtAl2009,
    1.76 +  editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
    1.77 +  title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
    1.78 +  booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
    1.79 +  series = "LNCS 5497",
    1.80 +  publisher = "Springer",
    1.81 +  year = 2009
    1.82 +}
    1.83 +
    1.84 +% MKM 2006
    1.85 +
    1.86 +@inproceedings{Ballarin2006b,
    1.87 +  author = "Clemens Ballarin",
    1.88 +  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
    1.89 +  pages = "31--43",
    1.90 +  crossref = "BorweinFarmer2006"
    1.91 +}
    1.92 +
    1.93 +@proceedings{BorweinFarmer2006,
    1.94 +  editor = "Jonathan M. Borwein and William M. Farmer",
    1.95 +  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
    1.96 +  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
    1.97 +  series = "LNCS 4108",
    1.98 +  publisher = "Springer",
    1.99 +  year = 2006,
   1.100 +  available = { CB }
   1.101 +}
   1.102 +
   1.103 +% TPHOLs 1999
   1.104 +
   1.105 +@inproceedings{KammullerEtAl1999,
   1.106 +  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
   1.107 +  title = "Locales: A Sectioning Concept for {Isabelle}",
   1.108 +  pages = "149--165",
   1.109 +  crossref = "BertotEtAl1999",
   1.110 +  available = { CB }
   1.111 +}
   1.112 +
   1.113 +@book{BertotEtAl1999,
   1.114 +  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
   1.115 +  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
   1.116 +  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
   1.117 +  publisher = "Springer",
   1.118 +  series = "LNCS 1690",
   1.119 +  year = 1999
   1.120 +}