|
1 @phdthesis{Bailey1998, |
|
2 author = "Anthony Bailey", |
|
3 title = "The machine-checked literate formalisation of algebra in type theory", |
|
4 school = "University of Manchester", |
|
5 month = jan, |
|
6 year = 1998, |
|
7 available = { CB } |
|
8 } |
|
9 |
|
10 @phdthesis{Kammuller1999a, |
|
11 author = "Florian Kamm{\"u}ller", |
|
12 title = "Modular Reasoning in {Isabelle}", |
|
13 school = "University of Cambridge, Computer Laboratory", |
|
14 note = "Available as Technical Report No. 470.", |
|
15 month = aug, |
|
16 year = 1999, |
|
17 available = { CB } |
|
18 } |
|
19 |
|
20 % TYPES 98 |
|
21 |
|
22 @inproceedings{Kammuller1999b, |
|
23 author = "Florian Kamm{\"u}ller", |
|
24 title = "Modular Structures as Dependent Types in {Isabelle}", |
|
25 pages = "121--132", |
|
26 crossref = "AltenkirchEtAl1999", |
|
27 available = { CB } |
|
28 } |
|
29 |
|
30 @proceedings{AltenkirchEtAl1999, |
|
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", |
|
36 number = 1657, |
|
37 year = 1999 |
|
38 } |
|
39 % CADE-17 |
|
40 |
|
41 @inproceedings{Kammuller2000, |
|
42 author = "Florian Kamm{\"u}ller", |
|
43 title = "Modular Reasoning in {Isabelle}", |
|
44 pages = "99--114", |
|
45 crossref = "McAllester2000", |
|
46 available = { CB } |
|
47 } |
|
48 |
|
49 @proceedings{McAllester2000, |
|
50 editor = "David McAllester", |
|
51 title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings", |
|
52 booktitle = "CADE 17", |
|
53 publisher = "Springer", |
|
54 series = "LNCS", |
|
55 number = 1831, |
|
56 year = 2000 |
|
57 } |
|
58 |
|
59 @book{NipkowEtAl2002, |
|
60 author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel", |
|
61 title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic", |
|
62 publisher = "Springer", |
|
63 series = "LNCS", |
|
64 number = 2283, |
|
65 year = 2002, |
|
66 available = { CB } |
|
67 } |
|
68 |
|
69 % TYPES 2002 |
|
70 |
|
71 @inproceedings{Nipkow2003, |
|
72 author = "Tobias Nipkow", |
|
73 title = "Structured Proofs in {Isar/HOL}", |
|
74 pages = "259--278", |
|
75 crossref = "GeuversWiedijk2003" |
|
76 } |
|
77 |
|
78 @proceedings{GeuversWiedijk2003, |
|
79 editor = "H. Geuvers and F. Wiedijk", |
|
80 title = "Types for Proofs and Programs (TYPES 2002)", |
|
81 booktitle = "TYPES 2002", |
|
82 publisher = "Springer", |
|
83 series = "LNCS", |
|
84 number = 2646, |
|
85 year = 2003 |
|
86 } |
|
87 |
|
88 @phdthesis{Wenzel2002a, |
|
89 author = "Markus Wenzel", |
|
90 title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents", |
|
91 school = "Technische Universit{\"a}t M{\"u}nchen", |
|
92 note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.", |
|
93 year = 2002 |
|
94 } |
|
95 |
|
96 @unpublished{Wenzel2002b, |
|
97 author = "Markus Wenzel", |
|
98 title = "Using locales in {Isabelle/Isar}", |
|
99 note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy. Distribution of Isabelle available at http://isabelle.in.tum.de", |
|
100 year = 2002 |
|
101 } |
|
102 |
|
103 @unpublished{Wenzel2003, |
|
104 author = "Markus Wenzel", |
|
105 title = "The {Isabelle/Isar} Reference Manual", |
|
106 note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de", |
|
107 year = 2003 |
|
108 } |
|
109 |
|
110 % TPHOLs 2003 |
|
111 |
|
112 @inproceedings{Chrzaszcz2003, |
|
113 author = "Jacek Chrzaszcz", |
|
114 title = "Implementing Modules in the {Coq} System", |
|
115 pages = "270--286", |
|
116 crossref = "BasinWolff2003", |
|
117 available = { CB } |
|
118 } |
|
119 |
|
120 @proceedings{BasinWolff2003, |
|
121 editor = "David Basin and Burkhart Wolff", |
|
122 title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings", |
|
123 booktitle = "TPHOLs 2003", |
|
124 publisher = "Springer", |
|
125 series = "LNCS", |
|
126 number = 2758, |
|
127 year = 2003 |
|
128 } |
|
129 |
|
130 @PhdThesis{Klein2003, |
|
131 author = "Gerwin Klein", |
|
132 title = "Verified Java Bytecode Verification", |
|
133 school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen", |
|
134 year = 2003 |
|
135 } |
|
136 |
|
137 % TACAS 2000 |
|
138 |
|
139 @inproceedings{Aspinall2000, |
|
140 author = "David Aspinall", |
|
141 title = "Proof General: A Generic Tool for Proof Development", |
|
142 pages = "38--42", |
|
143 crossref = "GrafSchwartzbach2000" |
|
144 } |
|
145 |
|
146 @proceedings{GrafSchwartzbach2000, |
|
147 editor = {Susanne Graf and Michael I. Schwartzbach}, |
|
148 title = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings}, |
|
149 booktitle = "TACAS 2000", |
|
150 publisher = {Springer}, |
|
151 series = {LNCS}, |
|
152 number = {1785}, |
|
153 year = {2000}, |
|
154 } |