1 @phdthesis{Bailey1998, |
1 @unpublished{IsarRef, |
2 author = "Anthony Bailey", |
2 author = "Markus Wenzel", |
3 title = "The machine-checked literate formalisation of algebra in type theory", |
3 title = "The {Isabelle/Isar} Reference Manual", |
4 school = "University of Manchester", |
4 note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}." |
5 month = jan, |
5 } |
6 year = 1998, |
6 |
|
7 @book {Jacobson1985, |
|
8 author = "Nathan Jacobson", |
|
9 title = "Basic Algebra", |
|
10 volume = "I", |
|
11 publisher = "Freeman", |
|
12 edition = "2nd", |
|
13 year = 1985, |
7 available = { CB } |
14 available = { CB } |
8 } |
15 } |
9 |
16 |
10 @phdthesis{Kammuller1999a, |
17 % TYPES 2006 |
11 author = "Florian Kamm{\"u}ller", |
18 |
12 title = "Modular Reasoning in {Isabelle}", |
19 @inproceedings{HaftmannWenzel2007, |
13 school = "University of Cambridge, Computer Laboratory", |
20 author = "Florian Haftmann and Makarius Wenzel", |
14 note = "Available as Technical Report No. 470.", |
21 title = "Constructive Type Classes in {Isabelle}", |
15 month = aug, |
22 pages = "160--174", |
16 year = 1999, |
23 crossref = "AltenkirchMcBride2007", |
17 available = { CB } |
24 available = { CB } |
18 } |
25 } |
19 |
26 |
20 % TYPES 98 |
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 } |
21 |
35 |
22 @inproceedings{Kammuller1999b, |
36 |
23 author = "Florian Kamm{\"u}ller", |
37 @techreport{Ballarin2006a, |
24 title = "Modular Structures as Dependent Types in {Isabelle}", |
38 author = "Clemens Ballarin", |
25 pages = "121--132", |
39 title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales", |
26 crossref = "AltenkirchEtAl1999", |
40 institution = "Technische Universit{\"a}t M{\"u}nchen", |
|
41 number = "TUM-I0607", |
|
42 year = 2006 |
|
43 } |
|
44 |
|
45 % MKM 2006 |
|
46 |
|
47 @inproceedings{Ballarin2006b, |
|
48 author = "Clemens Ballarin", |
|
49 title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts", |
|
50 pages = "31--43", |
|
51 crossref = "BorweinFarmer2006" |
|
52 } |
|
53 |
|
54 @proceedings{BorweinFarmer2006, |
|
55 editor = "Jonathan M. Borwein and William M. Farmer", |
|
56 title = "Mathematical knowledge management, MKM 2006, Wokingham, UK", |
|
57 booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK", |
|
58 series = "LNCS 4108", |
|
59 publisher = "Springer", |
|
60 year = 2006, |
27 available = { CB } |
61 available = { CB } |
28 } |
62 } |
29 |
63 |
30 @proceedings{AltenkirchEtAl1999, |
64 % TPHOLs 1999 |
31 editor = "Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus", |
|
32 title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers", |
|
33 booktitle = "TYPES '98", |
|
34 publisher = "Springer", |
|
35 series = "LNCS 1657", |
|
36 year = 1999 |
|
37 } |
|
38 % CADE-17 |
|
39 |
65 |
40 @inproceedings{Kammuller2000, |
66 @inproceedings{KammullerEtAl1999, |
41 author = "Florian Kamm{\"u}ller", |
67 author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson", |
42 title = "Modular Reasoning in {Isabelle}", |
68 title = "Locales: A Sectioning Concept for {Isabelle}", |
43 pages = "99--114", |
69 pages = "149--165", |
44 crossref = "McAllester2000", |
70 crossref = "BertotEtAl1999", |
45 available = { CB } |
71 available = { CB } |
46 } |
72 } |
47 |
73 |
48 @proceedings{McAllester2000, |
74 @book{BertotEtAl1999, |
49 editor = "David McAllester", |
75 editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry", |
50 title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings", |
76 title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France", |
51 booktitle = "CADE 17", |
77 booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France", |
52 publisher = "Springer", |
78 publisher = "Springer", |
53 series = "LNCS 1831", |
79 series = "LNCS 1690", |
54 year = 2000 |
80 year = 1999 |
55 } |
81 } |
56 |
|
57 @book{NipkowEtAl2002, |
|
58 author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel", |
|
59 title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic", |
|
60 publisher = "Springer", |
|
61 series = "LNCS 2283", |
|
62 year = 2002, |
|
63 available = { CB } |
|
64 } |
|
65 |
|
66 % TYPES 2002 |
|
67 |
|
68 @inproceedings{Nipkow2003, |
|
69 author = "Tobias Nipkow", |
|
70 title = "Structured Proofs in {Isar/HOL}", |
|
71 pages = "259--278", |
|
72 crossref = "GeuversWiedijk2003" |
|
73 } |
|
74 |
|
75 @proceedings{GeuversWiedijk2003, |
|
76 editor = "H. Geuvers and F. Wiedijk", |
|
77 title = "Types for Proofs and Programs (TYPES 2002)", |
|
78 booktitle = "TYPES 2002", |
|
79 publisher = "Springer", |
|
80 series = "LNCS 2646", |
|
81 year = 2003 |
|
82 } |
|
83 |
|
84 @phdthesis{Wenzel2002a, |
|
85 author = "Markus Wenzel", |
|
86 title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents", |
|
87 school = "Technische Universit{\"a}t M{\"u}nchen", |
|
88 note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.", |
|
89 year = 2002 |
|
90 } |
|
91 |
|
92 @unpublished{Wenzel2002b, |
|
93 author = "Markus Wenzel", |
|
94 title = "Using locales in {Isabelle/Isar}", |
|
95 note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy. Distribution of Isabelle available at http://isabelle.in.tum.de", |
|
96 year = 2002 |
|
97 } |
|
98 |
|
99 @unpublished{Wenzel2003, |
|
100 author = "Markus Wenzel", |
|
101 title = "The {Isabelle/Isar} Reference Manual", |
|
102 note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de", |
|
103 year = 2003 |
|
104 } |
|
105 |
|
106 % TPHOLs 2003 |
|
107 |
|
108 @inproceedings{Chrzaszcz2003, |
|
109 author = "Jacek Chrz{\c{a}}szcz", |
|
110 title = "Implementing Modules in the {Coq} System", |
|
111 pages = "270--286", |
|
112 crossref = "BasinWolff2003", |
|
113 available = { CB } |
|
114 } |
|
115 |
|
116 @proceedings{BasinWolff2003, |
|
117 editor = "David Basin and Burkhart Wolff", |
|
118 title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings", |
|
119 booktitle = "TPHOLs 2003", |
|
120 publisher = "Springer", |
|
121 series = "LNCS 2758", |
|
122 year = 2003 |
|
123 } |
|
124 |
|
125 @PhdThesis{Klein2003, |
|
126 author = "Gerwin Klein", |
|
127 title = "Verified Java Bytecode Verification", |
|
128 school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen", |
|
129 year = 2003 |
|
130 } |
|
131 |
|
132 % TACAS 2000 |
|
133 |
|
134 @inproceedings{Aspinall2000, |
|
135 author = "David Aspinall", |
|
136 title = "Proof General: A Generic Tool for Proof Development", |
|
137 pages = "38--42", |
|
138 crossref = "GrafSchwartzbach2000" |
|
139 } |
|
140 |
|
141 @proceedings{GrafSchwartzbach2000, |
|
142 editor = {Susanne Graf and Michael I. Schwartzbach}, |
|
143 title = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings}, |
|
144 booktitle = "TACAS 2000", |
|
145 publisher = {Springer}, |
|
146 series = {LNCS 1785}, |
|
147 year = {2000}, |
|
148 } |
|
149 |
|
150 % TYPES 2004 |
|
151 |
|
152 @inproceedings{Ballarin2004a, |
|
153 author = "Clemens Ballarin", |
|
154 title = "Locales and Locale Expressions in {Isabelle/Isar}", |
|
155 pages = "34--50", |
|
156 crossref = "BerardiEtAl2004" |
|
157 } |
|
158 |
|
159 @inproceedings{Chrzaszcz2004, |
|
160 author = "Jacek Chrz{\c{a}}szcz", |
|
161 title = "Modules in {Coq} Are and Will Be Correct", |
|
162 pages = "130--136", |
|
163 crossref = "BerardiEtAl2004", |
|
164 available = { CB } |
|
165 } |
|
166 @proceedings{BerardiEtAl2004, |
|
167 editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani", |
|
168 title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy", |
|
169 booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy", |
|
170 publisher = "Springer", |
|
171 series = "LNCS 3085", |
|
172 year = 2004 |
|
173 } |
|