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