author  haftmann 
Tue, 13 Jul 2010 11:38:04 +0200  
changeset 37788  261c61fabc98 
parent 37429  2f064f1c2f14 
child 38437  ffb1c5bf0425 
permissions  rwrr 
6592  1 
% BibTeX database for the Isabelle documentation 
2 

3 
%publishers 

4 
@string{AP="Academic Press"} 

5 
@string{CUP="Cambridge University Press"} 

35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
33926
diff
changeset

6 
@string{IEEE="IEEE Computer Society Press"} 
11199  7 
@string{LNCS="Lecture Notes in Computer Science"} 
6592  8 
@string{MIT="MIT Press"} 
9 
@string{NH="NorthHolland"} 

10 
@string{Prentice="PrenticeHall"} 

6607  11 
@string{PH="PrenticeHall"} 
6592  12 
@string{Springer="SpringerVerlag"} 
13 

14 
%institutions 

11199  15 
@string{CUCL="Computer Laboratory, University of Cambridge"} 
16 
@string{Edinburgh="Department of Computer Science, University of Edinburgh"} 

21074  17 
@string{TUM="Department of Informatics, Technical University of Munich"} 
6592  18 

19 
%journals 

8284  20 
@string{AI="Artificial Intelligence"} 
11199  21 
@string{FAC="Formal Aspects of Computing"} 
22 
@string{JAR="Journal of Automated Reasoning"} 

23 
@string{JCS="Journal of Computer Security"} 

24 
@string{JFP="Journal of Functional Programming"} 

25 
@string{JLC="Journal of Logic and Computation"} 

26 
@string{JLP="Journal of Logic Programming"} 

27 
@string{JSC="Journal of Symbolic Computation"} 

28 
@string{JSL="Journal of Symbolic Logic"} 

11246  29 
@string{PROYAL="Proceedings of the Royal Society of London"} 
6592  30 
@string{SIGPLAN="{SIGPLAN} Notices"} 
11246  31 
@string{TISSEC="ACM Transactions on Information and System Security"} 
6592  32 

33 
%conferences 

34 
@string{CADE="International Conference on Automated Deduction"} 

35 
@string{POPL="Symposium on Principles of Programming Languages"} 

36 
@string{TYPES="Types for Proofs and Programs"} 

37 

38 

39 
%A 

40 

41 
@incollection{abramsky90, 

42 
author = {Samson Abramsky}, 

43 
title = {The Lazy Lambda Calculus}, 

44 
pages = {65116}, 

45 
editor = {David A. Turner}, 

46 
booktitle = {Research Topics in Functional Programming}, 

47 
publisher = {AddisonWesley}, 

48 
year = 1990} 

49 

50 
@Unpublished{abrial93, 

51 
author = {J. R. Abrial and G. Laffitte}, 

33191  52 
title = {Towards the Mechanization of the Proofs of Some Classical 
6592  53 
Theorems of Set Theory}, 
54 
note = {preprint}, 

55 
year = 1993, 

56 
month = Feb} 

57 

58 
@incollection{aczel77, 

59 
author = {Peter Aczel}, 

60 
title = {An Introduction to Inductive Definitions}, 

61 
pages = {739782}, 

62 
crossref = {barwisehandbk}} 

63 

64 
@Book{aczel88, 

65 
author = {Peter Aczel}, 

66 
title = {NonWellFounded Sets}, 

67 
publisher = {CSLI}, 

68 
year = 1988} 

69 

70 
@InProceedings{alf, 

71 
author = {Lena Magnusson and Bengt {Nordstr\"{o}m}}, 

72 
title = {The {ALF} Proof Editor and Its Proof Engine}, 

73 
crossref = {types93}, 

74 
pages = {213237}} 

75 

33191  76 
@inproceedings{andersson1993, 
77 
author = "Arne Andersson", 

78 
title = "Balanced Search Trees Made Simple", 

79 
editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides", 

80 
booktitle = "WADS 1993", 

81 
series = LNCS, 

82 
volume = {709}, 

83 
pages = "6170", 

84 
year = 1993, 

85 
publisher = Springer} 

86 

6592  87 
@book{andrews86, 
88 
author = "Peter Andrews", 

89 
title = "An Introduction to Mathematical Logic and Type Theory: to Truth 

90 
through Proof", 

91 
publisher = AP, 

92 
series = "Computer Science and Applied Mathematics", 

93 
year = 1986} 

94 

9599  95 
@InProceedings{Aspinall:2000:eProof, 
96 
author = {David Aspinall}, 

97 
title = {Protocols for Interactive {eProof}}, 

98 
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, 

99 
year = 2000, 

100 
note = {Unpublished workinprogress paper, 

14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

101 
\url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}} 
9599  102 
} 
14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

103 

8505  104 
@InProceedings{Aspinall:TACAS:2000, 
105 
author = {David Aspinall}, 

10160  106 
title = {{P}roof {G}eneral: A Generic Tool for Proof Development}, 
11205  107 
booktitle = {Tools and Algorithms for the Construction and Analysis of 
108 
Systems (TACAS)}, 

109 
year = 2000, 

110 
publisher = Springer, 

111 
series = LNCS, 

112 
volume = 1785, 

113 
pages = "3842" 

8505  114 
} 
115 

7209  116 
@Misc{isamode, 
117 
author = {David Aspinall}, 

8062  118 
title = {Isamode  {U}sing {I}sabelle with {E}macs}, 
14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

119 
note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}} 
7209  120 
} 
121 

122 
@Misc{proofgeneral, 

11197  123 
author = {David Aspinall}, 
124 
title = {{P}roof {G}eneral}, 

14296
bcba1d67f854
updated references to the nowpornographic proofgeneral.org
paulson
parents:
14210
diff
changeset

125 
note = {\url{http://proofgeneral.inf.ed.ac.uk/}} 
7209  126 
} 
127 

6592  128 
%B 
129 

10186  130 
@book{BaaderNipkow,author={Franz Baader and Tobias Nipkow}, 
131 
title="Term Rewriting and All That",publisher=CUP,year=1998} 

132 

37429  133 
@manual{isabellelocale, 
134 
author = {Clemens Ballarin}, 

135 
title = {Tutorial to Locales and Locale Interpretation}, 

136 
institution = TUM, 

137 
note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} 

138 
} 

139 

20482  140 
@InCollection{BarendregtGeuvers:2001, 
141 
author = {H. Barendregt and H. Geuvers}, 

142 
title = {Proof Assistants using Dependent Type Systems}, 

143 
booktitle = {Handbook of Automated Reasoning}, 

144 
publisher = {Elsevier}, 

145 
year = 2001, 

146 
editor = {A. Robinson and A. Voronkov} 

147 
} 

148 

6592  149 
@incollection{basin91, 
150 
author = {David Basin and Matt Kaufmann}, 

151 
title = {The {BoyerMoore} Prover and {Nuprl}: An Experimental 

152 
Comparison}, 

153 
crossref = {huetplotkin91}, 

154 
pages = {89119}} 

155 

12466  156 
@Unpublished{HOLLibrary, 
157 
author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and 

158 
Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and 

159 
Markus Wenzel}, 

160 
title = {The Supplemental {Isabelle/HOL} Library}, 

12660  161 
note = {Part of the Isabelle distribution, 
12466  162 
\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, 
12660  163 
year = 2002 
12466  164 
} 
165 

9567  166 
@InProceedings{BauerWenzel:2000:HB, 
167 
author = {Gertrud Bauer and Markus Wenzel}, 

168 
title = {ComputerAssisted Mathematics at Work  The {H}ahn{B}anach Theorem in 

169 
{I}sabelle/{I}sar}, 

170 
booktitle = {Types for Proofs and Programs: TYPES'99}, 

9599  171 
editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m 
172 
and Jan Smith}, 

9567  173 
series = {LNCS}, 
9599  174 
year = 2000 
9567  175 
} 
6624  176 

12878  177 
@InProceedings{BauerWenzel:2001, 
178 
author = {Gertrud Bauer and Markus Wenzel}, 

179 
title = {Calculational reasoning revisited  an {Isabelle/Isar} experience}, 

180 
crossref = {tphols2001}} 

181 

33926
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

182 
@inProceedings{BerghoferBulwahnHaftmann:2009:TPHOL, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

183 
author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

184 
booktitle = {Theorem Proving in Higher Order Logics}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

185 
pages = {131146}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

186 
title = {Turning Inductive into Equational Specifications}, 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

187 
year = {2009} 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

188 
} 
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
33856
diff
changeset

189 

11619  190 
@INPROCEEDINGS{BerghoferNipkow:2000:TPHOL, 
191 
crossref = "tphols2000", 

192 
title = "Proof terms for simply typed higher order logic", 

193 
author = "Stefan Berghofer and Tobias Nipkow", 

194 
pages = "3852"} 

195 

33191  196 
@inproceedings{berghofernipkow2004, 
197 
author = {Stefan Berghofer and Tobias Nipkow}, 

198 
title = {Random Testing in {I}sabelle/{HOL}}, 

199 
pages = {230239}, 

200 
editor = "J. Cuellar and Z. Liu", 

201 
booktitle = {{SEFM} 2004}, 

202 
publisher = IEEE, 

203 
year = 2004} 

204 

12612  205 
@InProceedings{BerghoferNipkow:2002, 
206 
author = {Stefan Berghofer and Tobias Nipkow}, 

207 
title = {Executing Higher Order Logic}, 

208 
booktitle = {Types for Proofs and Programs: TYPES'2000}, 

209 
editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, 

210 
series = LNCS, 

211 
publisher = Springer, 

13009  212 
volume = 2277, 
12612  213 
year = 2002} 
214 

6624  215 
@InProceedings{BerghoferWenzel:1999:TPHOL, 
216 
author = {Stefan Berghofer and Markus Wenzel}, 

7041  217 
title = {Inductive datatypes in {HOL}  lessons learned in 
218 
{F}ormal{L}ogic {E}ngineering}, 

219 
crossref = {tphols99}} 

6624  220 

30170  221 

222 
@InProceedings{BezemCoquand:2005, 

223 
author = {M.A. Bezem and T. Coquand}, 

224 
title = {Automating {Coherent Logic}}, 

225 
booktitle = {LPAR12}, 

226 
editor = {G. Sutcliffe and A. Voronkov}, 

227 
volume = 3835, 

228 
series = LNCS, 

229 
publisher = Springer} 

230 

6607  231 
@book{BirdWadler,author="Richard Bird and Philip Wadler", 
232 
title="Introduction to Functional Programming",publisher=PH,year=1988} 

233 

11209  234 
@book{BirdHaskell,author="Richard Bird", 
235 
title="Introduction to Functional Programming using Haskell", 

236 
publisher=PH,year=1998} 

237 

36926  238 
@inproceedings{blanchettenipkow2010, 
239 
title = "Nitpick: A Counterexample Generator for HigherOrder Logic Based on a Relational Model Finder", 

33191  240 
author = "Jasmin Christian Blanchette and Tobias Nipkow", 
36926  241 
crossref = {itp2010}} 
242 

243 
@inproceedings{boehmenipkow2010, 

244 
author={Sascha B\"ohme and Tobias Nipkow}, 

245 
title={Sledgehammer: Judgement Day}, 

246 
booktitle={Automated Reasoning: IJCAR 2010}, 

247 
editor={J. Giesl and R. H\"ahnle}, 

248 
publisher=Springer, 

249 
series=LNCS, 

250 
year=2010} 

33191  251 

6592  252 
@Article{boyer86, 
253 
author = {Robert Boyer and Ewing Lusk and William McCune and Ross 

254 
Overbeek and Mark Stickel and Lawrence Wos}, 

255 
title = {Set Theory in FirstOrder Logic: Clauses for {G\"{o}del's} 

256 
Axioms}, 

257 
journal = JAR, 

258 
year = 1986, 

259 
volume = 2, 

260 
number = 3, 

261 
pages = {287327}} 

262 

263 
@book{bm79, 

264 
author = {Robert S. Boyer and J Strother Moore}, 

265 
title = {A Computational Logic}, 

266 
publisher = {Academic Press}, 

267 
year = 1979} 

268 

269 
@book{bm88book, 

270 
author = {Robert S. Boyer and J Strother Moore}, 

271 
title = {A Computational Logic Handbook}, 

272 
publisher = {Academic Press}, 

273 
year = 1988} 

274 

275 
@Article{debruijn72, 

276 
author = {N. G. de Bruijn}, 

277 
title = {Lambda Calculus Notation with Nameless Dummies, 

278 
a Tool for Automatic Formula Manipulation, 

279 
with Application to the {ChurchRosser Theorem}}, 

280 
journal = {Indag. Math.}, 

281 
volume = 34, 

282 
pages = {381392}, 

283 
year = 1972} 

284 

23187  285 
@InProceedings{bulwahnKN07, 
25093  286 
author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow}, 
287 
title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}}, 

288 
crossref = {tphols2007}, 

289 
pages = {3853} 

290 
} 

23187  291 

28593  292 
@InProceedings{bulwahnetal:2008:imperative, 
33191  293 
author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent ErkÃ¶k and John Matthews}, 
28593  294 
title = {Imperative Functional Programming with {Isabelle/HOL}}, 
295 
crossref = {tphols2008}, 

296 
} 

297 
% pages = {3853} 

298 

11246  299 
@Article{ban89, 
300 
author = {M. Burrows and M. Abadi and R. M. Needham}, 

301 
title = {A Logic of Authentication}, 

302 
journal = PROYAL, 

303 
year = 1989, 

304 
volume = 426, 

305 
pages = {233271}} 

306 

6592  307 
%C 
308 

309 
@TechReport{camilleri92, 

310 
author = {J. Camilleri and T. F. Melham}, 

311 
title = {Reasoning with Inductively Defined Relations in the 

312 
{HOL} Theorem Prover}, 

313 
institution = CUCL, 

314 
year = 1992, 

315 
number = 265, 

316 
month = Aug} 

317 

318 
@Book{charniak80, 

319 
author = {E. Charniak and C. K. Riesbeck and D. V. McDermott}, 

320 
title = {Artificial Intelligence Programming}, 

321 
publisher = {Lawrence Erlbaum Associates}, 

322 
year = 1980} 

323 

324 
@article{church40, 

325 
author = "Alonzo Church", 

326 
title = "A Formulation of the Simple Theory of Types", 

327 
journal = JSL, 

328 
year = 1940, 

329 
volume = 5, 

330 
pages = "5668"} 

331 

10191  332 
@book{ClarkeGPbook,author="Edmund Clarke and Orna Grumberg and Doron Peled", 
333 
title="Model Checking",publisher=MIT,year=1999} 

334 

6592  335 
@PhdThesis{coen92, 
336 
author = {Martin D. Coen}, 

337 
title = {Interactive Program Derivation}, 

338 
school = {University of Cambridge}, 

339 
note = {Computer Laboratory Technical Report 272}, 

340 
month = nov, 

341 
year = 1992} 

342 

343 
@book{constable86, 

344 
author = {R. L. Constable and others}, 

345 
title = {Implementing Mathematics with the Nuprl Proof 

346 
Development System}, 

347 
publisher = Prentice, 

348 
year = 1986} 

349 

350 
%D 

351 

6745  352 
@Book{daveypriestley, 
6592  353 
author = {B. A. Davey and H. A. Priestley}, 
354 
title = {Introduction to Lattices and Order}, 

355 
publisher = CUP, 

356 
year = 1990} 

357 

358 
@Book{devlin79, 

359 
author = {Keith J. Devlin}, 

360 
title = {Fundamentals of Contemporary Set Theory}, 

361 
publisher = {Springer}, 

362 
year = 1979} 

363 

364 
@book{dummett, 

365 
author = {Michael Dummett}, 

366 
title = {Elements of Intuitionism}, 

367 
year = 1977, 

368 
publisher = {Oxford University Press}} 

369 

370 
@incollection{dybjer91, 

371 
author = {Peter Dybjer}, 

10186  372 
title = {Inductive Sets and Families in {MartinL{\"o}f's} Type 
6592  373 
Theory and Their SetTheoretic Semantics}, 
374 
crossref = {huetplotkin91}, 

375 
pages = {280306}} 

376 

377 
@Article{dyckhoff, 

378 
author = {Roy Dyckhoff}, 

379 
title = {ContractionFree Sequent Calculi for Intuitionistic Logic}, 

380 
journal = JSL, 

381 
year = 1992, 

382 
volume = 57, 

383 
number = 3, 

384 
pages = {795807}} 

385 

386 
%F 

387 

6613
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

388 
@Article{IMPS, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

389 
author = {William M. Farmer and Joshua D. Guttman and F. Javier 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

390 
Thayer}, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

391 
title = {{IMPS}: An Interactive Mathematical Proof System}, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

392 
journal = JAR, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

393 
volume = 11, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

394 
number = 2, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

395 
year = 1993, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

396 
pages = {213248}} 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

397 

6592  398 
@InProceedings{felty91a, 
399 
Author = {Amy Felty}, 

400 
Title = {A Logic Program for Transforming Sequent Proofs to Natural 

401 
Deduction Proofs}, 

402 
crossref = {extensions91}, 

403 
pages = {157178}} 

404 

10796  405 
@Article{fleuriotjcm, 
406 
author = {Jacques Fleuriot and Lawrence C. Paulson}, 

407 
title = {Mechanizing Nonstandard Real Analysis}, 

408 
journal = {LMS Journal of Computation and Mathematics}, 

409 
year = 2000, 

410 
volume = 3, 

411 
pages = {140190}, 

412 
note = {\url{http://www.lms.ac.uk/jcm/3/lms1999027/}} 

413 
} 

414 

6592  415 
@TechReport{frost93, 
416 
author = {Jacob Frost}, 

417 
title = {A Case Study of Coinduction in {Isabelle HOL}}, 

418 
institution = CUCL, 

419 
number = 308, 

420 
year = 1993, 

421 
month = Aug} 

422 

423 
%revised version of frost93 

424 
@TechReport{frost95, 

425 
author = {Jacob Frost}, 

426 
title = {A Case Study of Coinduction in {Isabelle}}, 

427 
institution = CUCL, 

428 
number = 359, 

429 
year = 1995, 

430 
month = Feb} 

431 

432 
@inproceedings{OBJ, 

433 
author = {K. Futatsugi and J.A. Goguen and JeanPierre Jouannaud 

434 
and J. Meseguer}, 

435 
title = {Principles of {OBJ2}}, 

436 
booktitle = POPL, 

437 
year = 1985, 

438 
pages = {5266}} 

439 

440 
%G 

441 

442 
@book{gallier86, 

443 
author = {J. H. Gallier}, 

444 
title = {Logic for Computer Science: 

445 
Foundations of Automatic Theorem Proving}, 

446 
year = 1986, 

447 
publisher = {Harper \& Row}} 

448 

449 
@Book{galton90, 

450 
author = {Antony Galton}, 

451 
title = {Logic for Information Technology}, 

452 
publisher = {Wiley}, 

453 
year = 1990} 

454 

20506  455 
@Article{Gentzen:1935, 
456 
author = {G. Gentzen}, 

457 
title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en}, 

458 
journal = {Math. Zeitschrift}, 

459 
year = 1935 

460 
} 

461 

6592  462 
@InProceedings{gimenezcodifying, 
463 
author = {Eduardo Gim{\'e}nez}, 

464 
title = {Codifying Guarded Definitions with Recursive Schemes}, 

465 
crossref = {types94}, 

466 
pages = {3959} 

467 
} 

468 

9816  469 
@book{girard89, 
470 
author = {JeanYves Girard}, 

471 
title = {Proofs and Types}, 

472 
year = 1989, 

473 
publisher = CUP, 

474 
note = {Translated by Yves LaFont and Paul Taylor}} 

475 

6592  476 
@Book{mgordonhol, 
11205  477 
editor = {M. J. C. Gordon and T. F. Melham}, 
6592  478 
title = {Introduction to {HOL}: A Theorem Proving Environment for 
479 
Higher Order Logic}, 

480 
publisher = CUP, 

481 
year = 1993} 

482 

483 
@book{mgordon79, 

484 
author = {Michael J. C. Gordon and Robin Milner and Christopher P. 

485 
Wadsworth}, 

486 
title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, 

487 
year = 1979, 

488 
publisher = {Springer}, 

489 
series = {LNCS 78}} 

490 

6607  491 
@inproceedings{GunterHOL92,author={Elsa L. Gunter}, 
492 
title={Why we can't have {SML} style datatype declarations in {HOL}}, 

493 
booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\ 

494 
IFIP TC10/WG10.2 Intl. Workshop, 1992}, 

495 
editor={L.J.M. Claesen and M.J.C. Gordon}, 

496 
publisher=NH,year=1993,pages={561568}} 

497 

6592  498 
@InProceedings{guntertrees, 
499 
author = {Elsa L. Gunter}, 

500 
title = {A Broader Class of Trees for Recursive Type Definitions for 

501 
{HOL}}, 

502 
crossref = {hug93}, 

503 
pages = {141154}} 

504 

505 
%H 

506 

23956  507 
@InProceedings{HaftmannWenzel:2006:classes, 
508 
author = {Florian Haftmann and Makarius Wenzel}, 

509 
title = {Constructive Type Classes in {Isabelle}}, 

24628  510 
editor = {T. Altenkirch and C. McBride}, 
511 
booktitle = {Types for Proofs and Programs, TYPES 2006}, 

512 
publisher = {Springer}, 

513 
series = {LNCS}, 

514 
volume = {4502}, 

515 
year = {2007} 

24193  516 
} 
517 

37429  518 
@inproceedings{HaftmannNipkow:2010:code, 
519 
author = {Florian Haftmann and Tobias Nipkow}, 

520 
title = {Code Generation via HigherOrder Rewrite Systems}, 

521 
booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010}, 

522 
year = 2010, 

523 
publisher = {Springer}, 

524 
series = {Lecture Notes in Computer Science}, 

525 
editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal}, 

526 
volume = {6009} 

23956  527 
} 
528 

30115  529 
@InProceedings{HaftmannWenzel:2009, 
530 
author = {Florian Haftmann and Makarius Wenzel}, 

531 
title = {Local theory specifications in {Isabelle/Isar}}, 

532 
editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo}, 

533 
booktitle = {Types for Proofs and Programs, TYPES 2008}, 

534 
publisher = {Springer}, 

535 
series = {LNCS}, 

32572  536 
volume = {5497}, 
30115  537 
year = {2009} 
538 
} 

539 

22290  540 
@manual{isabelleclasses, 
24193  541 
author = {Florian Haftmann}, 
542 
title = {Haskellstyle type classes with {Isabelle}/{Isar}}, 

543 
institution = TUM, 

544 
note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}} 

545 
} 

22290  546 

547 
@manual{isabellecodegen, 

24193  548 
author = {Florian Haftmann}, 
549 
title = {Code generation from Isabelle theories}, 

550 
institution = TUM, 

551 
note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}} 

552 
} 

22290  553 

6592  554 
@Book{halmos60, 
555 
author = {Paul R. Halmos}, 

556 
title = {Naive Set Theory}, 

557 
publisher = {Van Nostrand}, 

558 
year = 1960} 

559 

11207  560 
@book{HarelKTDL,author={David Harel and Dexter Kozen and Jerzy Tiuryn}, 
561 
title={Dynamic Logic},publisher=MIT,year=2000} 

562 

6592  563 
@Book{hennessy90, 
564 
author = {Matthew Hennessy}, 

565 
title = {The Semantics of Programming Languages: An Elementary 

566 
Introduction Using Structural Operational Semantics}, 

567 
publisher = {Wiley}, 

568 
year = 1990} 

569 

10244  570 
@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman}, 
571 
title={Introduction to Automata Theory, Languages, and Computation.}, 

572 
publisher={AddisonWesley},year=1979} 

573 

6592  574 
@Article{haskellreport, 
575 
author = {Paul Hudak and Simon Peyton Jones and Philip Wadler}, 

576 
title = {Report on the Programming Language {Haskell}: A 

577 
Nonstrict, Purely Functional Language}, 

578 
journal = SIGPLAN, 

579 
year = 1992, 

580 
volume = 27, 

581 
number = 5, 

582 
month = May, 

583 
note = {Version 1.2}} 

584 

585 
@Article{haskelltutorial, 

586 
author = {Paul Hudak and Joseph H. Fasel}, 

587 
title = {A Gentle Introduction to {Haskell}}, 

588 
journal = SIGPLAN, 

589 
year = 1992, 

590 
volume = 27, 

591 
number = 5, 

592 
month = May} 

593 

11209  594 
@book{HudakHaskell,author={Paul Hudak}, 
595 
title={The Haskell School of Expression},publisher=CUP,year=2000} 

596 

6592  597 
@article{huet75, 
598 
author = {G. P. Huet}, 

599 
title = {A Unification Algorithm for Typed $\lambda$Calculus}, 

600 
journal = TCS, 

601 
volume = 1, 

602 
year = 1975, 

603 
pages = {2757}} 

604 

605 
@article{huet78, 

606 
author = {G. P. Huet and B. Lang}, 

607 
title = {Proving and Applying Program Transformations Expressed with 

608 
SecondOrder Patterns}, 

609 
journal = acta, 

610 
volume = 11, 

611 
year = 1978, 

612 
pages = {3155}} 

613 

614 
@inproceedings{huet88, 

10186  615 
author = {G{\'e}rard Huet}, 
6592  616 
title = {Induction Principles Formalized in the {Calculus of 
617 
Constructions}}, 

618 
booktitle = {Programming of Future Generation Computers}, 

619 
editor = {K. Fuchi and M. Nivat}, 

620 
year = 1988, 

621 
pages = {205216}, 

622 
publisher = {Elsevier}} 

623 

10186  624 
@Book{HuthRyanbook, 
625 
author = {Michael Huth and Mark Ryan}, 

626 
title = {Logic in Computer Science. Modelling and reasoning about systems}, 

627 
publisher = CUP, 

628 
year = 2000} 

629 

7041  630 
@InProceedings{Harrison:1996:MizarHOL, 
631 
author = {J. Harrison}, 

632 
title = {A {Mizar} Mode for {HOL}}, 

633 
pages = {203220}, 

634 
crossref = {tphols96}} 

635 

36926  636 
@misc{metis, 
637 
author = "Joe Hurd", 

638 
title = "Metis Theorem Prover", 

639 
note = "\url{http://www.gilith.com/software/metis/}"} 

640 

22290  641 
%J 
642 

643 
@article{haskellrevisedreport, 

644 
author = {Simon {Peyton Jones} and others}, 

645 
title = {The {Haskell} 98 Language and Libraries: The Revised Report}, 

646 
journal = {Journal of Functional Programming}, 

647 
volume = 13, 

648 
number = 1, 

649 
pages = {0255}, 

650 
month = {Jan}, 

651 
year = 2003, 

652 
note = {\url{http://www.haskell.org/definition/}}} 

653 

33191  654 
@book{jackson2006, 
655 
author = "Daniel Jackson", 

656 
title = "Software Abstractions: Logic, Language, and Analysis", 

657 
publisher = MIT, 

658 
year = 2006} 

659 

6592  660 
%K 
661 

6670  662 
@InProceedings{kammuellerlocales, 
663 
author = {Florian Kamm{\"u}ller and Markus Wenzel and 

664 
Lawrence C. Paulson}, 

665 
title = {Locales: A Sectioning Concept for {Isabelle}}, 

666 
crossref = {tphols99}} 

667 

8284  668 
@book{Knuth375, 
669 
author={Donald E. Knuth}, 

670 
title={The Art of Computer Programming, Volume 3: Sorting and Searching}, 

671 
publisher={AddisonWesley}, 

672 
year=1975} 

673 

674 
@Article{korf85, 

675 
author = {R. E. Korf}, 

676 
title = {DepthFirst IterativeDeepening: an Optimal Admissible 

677 
Tree Search}, 

678 
journal = AI, 

679 
year = 1985, 

680 
volume = 27, 

681 
pages = {97109}} 

6607  682 

23187  683 
@InProceedings{krauss2006, 
684 
author = {Alexander Krauss}, 

685 
title = {Partial Recursive Functions in {HigherOrder Logic}}, 

686 
crossref = {ijcar2006}, 

687 
pages = {589603}} 

688 

33856  689 
@PhdThesis{krauss_phd, 
690 
author = {Alexander Krauss}, 

691 
title = {Automating Recursive Definitions and Termination Proofs in HigherOrder Logic}, 

692 
school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, 

693 
year = {2009}, 

694 
address = {Germany} 

695 
} 

696 

24524  697 
@manual{isabellefunction, 
698 
author = {Alexander Krauss}, 

699 
title = {Defining Recursive Functions in {Isabelle/HOL}}, 

700 
institution = TUM, 

25280  701 
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} 
24524  702 
} 
703 

6592  704 
@Book{kunen80, 
705 
author = {Kenneth Kunen}, 

706 
title = {Set Theory: An Introduction to Independence Proofs}, 

707 
publisher = NH, 

708 
year = 1980} 

709 

11246  710 
%L 
711 

22290  712 
@manual{OCaml, 
713 
author = {Xavier Leroy and others}, 

714 
title = {The Objective Caml system  Documentation and user's manual}, 

715 
note = {\url{http://caml.inria.fr/pub/docs/manualocaml/}}} 

716 

11246  717 
@InProceedings{lowefdr, 
718 
author = {Gavin Lowe}, 

719 
title = {Breaking and Fixing the {Needham}{Schroeder} PublicKey 

720 
Protocol using {CSP} and {FDR}}, 

721 
booktitle = {Tools and Algorithms for the Construction and Analysis 

722 
of Systems: second international workshop, TACAS '96}, 

723 
editor = {T. Margaria and B. Steffen}, 

724 
series = {LNCS 1055}, 

725 
year = 1996, 

726 
publisher = {Springer}, 

727 
pages = {147166}} 

728 

6592  729 
%M 
730 

731 
@Article{mw81, 

732 
author = {Zohar Manna and Richard Waldinger}, 

733 
title = {Deductive Synthesis of the Unification Algorithm}, 

734 
journal = SCP, 

735 
year = 1981, 

736 
volume = 1, 

737 
number = 1, 

738 
pages = {548}} 

739 

740 
@InProceedings{martinnipkow, 

741 
author = {Ursula Martin and Tobias Nipkow}, 

742 
title = {Ordered Rewriting and Confluence}, 

743 
crossref = {cade10}, 

744 
pages = {366380}} 

745 

746 
@book{martinlof84, 

10186  747 
author = {Per MartinL{\"o}f}, 
6592  748 
title = {Intuitionistic type theory}, 
749 
year = 1984, 

750 
publisher = {Bibliopolis}} 

751 

752 
@incollection{melham89, 

753 
author = {Thomas F. Melham}, 

754 
title = {Automating Recursive Type Definitions in Higher Order 

755 
Logic}, 

756 
pages = {341386}, 

757 
crossref = {birtwistle89}} 

758 

29728  759 
@Article{Miller:1991, 
760 
author = {Dale Miller}, 

761 
title = {A Logic Programming Language with LambdaAbstraction, Function Variables, 

762 
and Simple Unification}, 

763 
journal = {Journal of Logic and Computation}, 

764 
year = 1991, 

765 
volume = 1, 

766 
number = 4 

767 
} 

768 

6592  769 
@Article{millermixed, 
770 
Author = {Dale Miller}, 

771 
Title = {Unification Under a Mixed Prefix}, 

772 
journal = JSC, 

773 
volume = 14, 

774 
number = 4, 

775 
pages = {321358}, 

776 
Year = 1992} 

777 

778 
@Article{milner78, 

779 
author = {Robin Milner}, 

780 
title = {A Theory of Type Polymorphism in Programming}, 

781 
journal = "J. Comp.\ Sys.\ Sci.", 

782 
year = 1978, 

783 
volume = 17, 

784 
pages = {348375}} 

785 

786 
@TechReport{milnerind, 

787 
author = {Robin Milner}, 

788 
title = {How to Derive Inductions in {LCF}}, 

789 
institution = Edinburgh, 

790 
year = 1980, 

791 
type = {note}} 

792 

793 
@Article{milnercoind, 

794 
author = {Robin Milner and Mads Tofte}, 

795 
title = {Coinduction in Relational Semantics}, 

796 
journal = TCS, 

797 
year = 1991, 

798 
volume = 87, 

799 
pages = {209220}} 

800 

801 
@Book{milner89, 

802 
author = {Robin Milner}, 

803 
title = {Communication and Concurrency}, 

804 
publisher = Prentice, 

805 
year = 1989} 

806 

10970  807 
@book{SML,author="Robin Milner and Mads Tofte and Robert Harper", 
808 
title="The Definition of Standard ML",publisher=MIT,year=1990} 

809 

6592  810 
@PhdThesis{monahan84, 
811 
author = {Brian Q. Monahan}, 

812 
title = {Data Type Proofs using Edinburgh {LCF}}, 

813 
school = {University of Edinburgh}, 

814 
year = 1984} 

815 

6607  816 
@article{MuellerNvOS99, 
817 
author= 

11564  818 
{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, 
11197  819 
title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191223}} 
6607  820 

9599  821 
@Manual{Muzalewski:Mizar, 
822 
title = {An Outline of {PC} {Mizar}}, 

823 
author = {Micha{\l} Muzalewski}, 

824 
organization = {Fondation of Logic, Mathematics and Informatics 

825 
 Mizar Users Group}, 

826 
year = 1993, 

827 
note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}} 

828 
} 

829 

6592  830 
%N 
831 

832 
@InProceedings{NaraschewskiWTPHOLs98, 

833 
author = {Wolfgang Naraschewski and Markus Wenzel}, 

834 
title = 

7041  835 
{ObjectOriented Verification based on Record Subtyping in 
836 
HigherOrder Logic}, 

837 
crossref = {tphols98}} 

6592  838 

839 
@inproceedings{nazarethnipkow, 

840 
author = {Dieter Nazareth and Tobias Nipkow}, 

841 
title = {Formal Verification of Algorithm {W}: The Monomorphic Case}, 

842 
crossref = {tphols96}, 

843 
pages = {331345}, 

844 
year = 1996} 

845 

11246  846 
@Article{needhamschroeder, 
847 
author = "Roger M. Needham and Michael D. Schroeder", 

848 
title = "Using Encryption for Authentication in Large Networks 

849 
of Computers", 

850 
journal = cacm, 

851 
volume = 21, 

852 
number = 12, 

853 
pages = "993999", 

854 
month = dec, 

855 
year = 1978} 

856 

6592  857 
@inproceedings{nipkowW, 
858 
author = {Wolfgang Naraschewski and Tobias Nipkow}, 

859 
title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}}, 

860 
booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96}, 

10186  861 
editor = {E. Gim{\'e}nez and C. PaulinMohring}, 
6592  862 
publisher = Springer, 
863 
series = LNCS, 

864 
volume = 1512, 

865 
pages = {317332}, 

866 
year = 1998} 

867 

8892  868 
@InCollection{nipkowsorts93, 
869 
author = {T. Nipkow}, 

870 
title = {OrderSorted Polymorphism in {Isabelle}}, 

871 
booktitle = {Logical Environments}, 

872 
publisher = CUP, 

873 
year = 1993, 

874 
editor = {G. Huet and G. Plotkin}, 

875 
pages = {164188} 

876 
} 

877 

878 
@Misc{nipkowtypes93, 

879 
author = {Tobias Nipkow}, 

880 
title = {Axiomatic Type Classes (in {I}sabelle)}, 

881 
howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen}, 

882 
year = 1993 

883 
} 

884 

6592  885 
@inproceedings{NipkowCR, 
886 
author = {Tobias Nipkow}, 

887 
title = {More {ChurchRosser} Proofs (in {Isabelle/HOL})}, 

888 
booktitle = {Automated Deduction  CADE13}, 

889 
editor = {M. McRobbie and J.K. Slaney}, 

890 
publisher = Springer, 

891 
series = LNCS, 

892 
volume = 1104, 

893 
pages = {733747}, 

894 
year = 1996} 

895 

896 
% WAS NipkowLICS93 

897 
@InProceedings{nipkowpatterns, 

898 
title = {Functional Unification of HigherOrder Patterns}, 

899 
author = {Tobias Nipkow}, 

900 
pages = {6474}, 

901 
crossref = {lics8}, 

6745  902 
url = {\url{ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/lics93.html}}, 
6592  903 
keywords = {unification}} 
904 

905 
@article{nipkowIMP, 

906 
author = {Tobias Nipkow}, 

907 
title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, 

908 
journal = FAC, 

909 
volume = 10, 

910 
pages = {171186}, 

911 
year = 1998} 

912 

15429  913 
@inproceedings{NipkowTYPES02, 
914 
author = {Tobias Nipkow}, 

915 
title = {{Structured Proofs in Isar/HOL}}, 

916 
booktitle = {Types for Proofs and Programs (TYPES 2002)}, 

917 
editor = {H. Geuvers and F. Wiedijk}, 

918 
year = 2003, 

919 
publisher = Springer, 

920 
series = LNCS, 

921 
volume = 2646, 

922 
pages = {259278}} 

923 

6607  924 
@manual{isabelleHOL, 
925 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

926 
title = {{Isabelle}'s Logics: {HOL}}, 

10186  927 
institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t 
928 
M{\"u}nchen and Computer Laboratory, University of Cambridge}, 

8892  929 
note = {\url{http://isabelle.in.tum.de/doc/logicsHOL.pdf}}} 
6607  930 

6592  931 
@article{nipkowprehofer, 
932 
author = {Tobias Nipkow and Christian Prehofer}, 

933 
title = {Type Reconstruction for Type Classes}, 

934 
journal = JFP, 

935 
volume = 5, 

936 
number = 2, 

937 
year = 1995, 

938 
pages = {201224}} 

939 

23956  940 
@InProceedings{NipkowPrehofer:1993, 
941 
author = {T. Nipkow and C. Prehofer}, 

942 
title = {Type checking type classes}, 

943 
booktitle = {ACM Symp.\ Principles of Programming Languages}, 

944 
year = 1993 

945 
} 

946 

14147  947 
@Book{isatutorial, 
948 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

33191  949 
title = {Isabelle/{HOL}: A Proof Assistant for HigherOrder Logic}, 
950 
publisher = Springer, 

14147  951 
year = 2002, 
33191  952 
series = LNCS, 
953 
volume = 2283} 

14147  954 

6592  955 
@Article{noel, 
956 
author = {Philippe No{\"e}l}, 

957 
title = {Experimenting with {Isabelle} in {ZF} Set Theory}, 

958 
journal = JAR, 

959 
volume = 10, 

960 
number = 1, 

961 
pages = {1558}, 

962 
year = 1993} 

963 

964 
@book{nordstrom90, 

10186  965 
author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith}, 
966 
title = {Programming in {MartinL{\"o}f}'s Type Theory. An 

6592  967 
Introduction}, 
968 
publisher = {Oxford University Press}, 

969 
year = 1990} 

970 

971 
%O 

972 

973 
@Manual{pvslanguage, 

974 
title = {The {PVS} specification language}, 

975 
author = {S. Owre and N. Shankar and J. M. Rushby}, 

976 
organization = {Computer Science Laboratory, SRI International}, 

977 
address = {Menlo Park, CA}, 

6745  978 
note = {Beta release}, 
6592  979 
year = 1993, 
980 
month = apr, 

6619  981 
url = {\url{http://www.csl.sri.com/reports/pvslanguage.dvi.Z}}} 
6592  982 

983 
%P 

984 

985 
% replaces paulin92 

986 
@InProceedings{paulintlca, 

987 
author = {Christine PaulinMohring}, 

988 
title = {Inductive Definitions in the System {Coq}: Rules and 

989 
Properties}, 

990 
crossref = {tlca93}, 

991 
pages = {328345}} 

992 

993 
@InProceedings{paulsonCADE, 

994 
author = {Lawrence C. Paulson}, 

995 
title = {A Fixedpoint Approach to Implementing (Co)Inductive 

996 
Definitions}, 

997 
pages = {148161}, 

998 
crossref = {cade12}} 

999 

1000 
@InProceedings{paulsonCOLOG, 

1001 
author = {Lawrence C. Paulson}, 

1002 
title = {A Formulation of the Simple Theory of Types (for 

1003 
{Isabelle})}, 

1004 
pages = {246274}, 

1005 
crossref = {colog88}, 

6619  1006 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175lcpsimple.dvi.gz}}} 
6592  1007 

1008 
@Article{paulsoncoind, 

1009 
author = {Lawrence C. Paulson}, 

1010 
title = {Mechanizing Coinduction and Corecursion in HigherOrder 

1011 
Logic}, 

1012 
journal = JLC, 

1013 
year = 1997, 

1014 
volume = 7, 

1015 
number = 2, 

1016 
month = mar, 

1017 
pages = {175204}} 

1018 

12616  1019 
@manual{isabelleintro, 
1020 
author = {Lawrence C. Paulson}, 

1021 
title = {Introduction to {Isabelle}}, 

1022 
institution = CUCL, 

1023 
note = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}} 

1024 

1025 
@manual{isabellelogics, 

1026 
author = {Lawrence C. Paulson}, 

1027 
title = {{Isabelle's} Logics}, 

1028 
institution = CUCL, 

1029 
note = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}} 

1030 

6613
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

1031 
@manual{isabelleref, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

1032 
author = {Lawrence C. Paulson}, 
250a0ca35ef5
new refererences for Inductive manual, but still incomplete
paulson
parents:
6607
diff
changeset

1033 
title = {The {Isabelle} Reference Manual}, 
8892  1034 
institution = CUCL, 
1035 
note = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}} 

6607  1036 

1037 
@manual{isabelleZF, 

6592  1038 
author = {Lawrence C. Paulson}, 
1039 
title = {{Isabelle}'s Logics: {FOL} and {ZF}}, 

8892  1040 
institution = CUCL, 
1041 
note = {\url{http://isabelle.in.tum.de/doc/logicsZF.pdf}}} 

6592  1042 

1043 
@article{paulsonfound, 

1044 
author = {Lawrence C. Paulson}, 

1045 
title = {The Foundation of a Generic Theorem Prover}, 

1046 
journal = JAR, 

1047 
volume = 5, 

1048 
number = 3, 

1049 
pages = {363397}, 

1050 
year = 1989, 

6619  1051 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130lcpgenerictheoremprover.dvi.gz}}} 
6592  1052 

1053 
%replaces paulsonfinal 

1054 
@Article{paulsonmscs, 

1055 
author = {Lawrence C. Paulson}, 

7991  1056 
title = {Final Coalgebras as Greatest Fixed Points 
1057 
in {ZF} Set Theory}, 

6592  1058 
journal = {Mathematical Structures in Computer Science}, 
1059 
year = 1999, 

1060 
volume = 9, 

23505  1061 
number = 5, 
1062 
pages = {545567}} 

6592  1063 

1064 
@InCollection{paulsongeneric, 

1065 
author = {Lawrence C. Paulson}, 

1066 
title = {Generic Automatic Proof Tools}, 

1067 
crossref = {wosfest}, 

1068 
chapter = 3} 

1069 

1070 
@Article{paulsongr, 

1071 
author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski}, 

1072 
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of 

1073 
Choice}, 

1074 
journal = JAR, 

1075 
year = 1996, 

1076 
volume = 17, 

1077 
number = 3, 

1078 
month = dec, 

1079 
pages = {291323}} 

1080 

14210  1081 
@InCollection{paulsonfixedptmilner, 
1082 
author = {Lawrence C. Paulson}, 

1083 
title = {A Fixedpoint Approach to (Co)inductive and 

1084 
(Co)datatype Definitions}, 

1085 
pages = {187211}, 

1086 
crossref = {milnerfest}} 

1087 

1088 
@book{milnerfest, 

1089 
title = {Proof, Language, and Interaction: 

1090 
Essays in Honor of {Robin Milner}}, 

1091 
booktitle = {Proof, Language, and Interaction: 

1092 
Essays in Honor of {Robin Milner}}, 

33191  1093 
publisher = MIT, 
14210  1094 
year = 2000, 
1095 
editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}} 

1096 

6592  1097 
@InCollection{paulsonhandbook, 
1098 
author = {Lawrence C. Paulson}, 

1099 
title = {Designing a Theorem Prover}, 

1100 
crossref = {handbklics2}, 

1101 
pages = {415475}} 

1102 

1103 
@Book{paulsonisabook, 

1104 
author = {Lawrence C. Paulson}, 

1105 
title = {Isabelle: A Generic Theorem Prover}, 

1106 
publisher = {Springer}, 

1107 
year = 1994, 

1108 
note = {LNCS 828}} 

1109 

12878  1110 
@Book{isabelleholbook, 
1111 
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, 

1112 
title = {Isabelle/HOL  A Proof Assistant for HigherOrder Logic}, 

1113 
publisher = {Springer}, 

1114 
year = 2002, 

1115 
note = {LNCS 2283}} 

1116 

6592  1117 
@InCollection{paulsonmarkt, 
1118 
author = {Lawrence C. Paulson}, 

1119 
title = {Tool Support for Logics of Programs}, 

1120 
booktitle = {Mathematical Methods in Program Development: 

1121 
Summer School Marktoberdorf 1996}, 

1122 
publisher = {Springer}, 

1123 
pages = {461498}, 

1124 
year = {Published 1997}, 

1125 
editor = {Manfred Broy}, 

1126 
series = {NATO ASI Series F}} 

1127 

1128 
%replaces PaulsonML and paulson91 

1129 
@book{paulsonml2, 

1130 
author = {Lawrence C. Paulson}, 

1131 
title = {{ML} for the Working Programmer}, 

1132 
year = 1996, 

1133 
edition = {2nd}, 

1134 
publisher = CUP} 

1135 

1136 
@article{paulsonnatural, 

1137 
author = {Lawrence C. Paulson}, 

1138 
title = {Natural Deduction as Higherorder Resolution}, 

1139 
journal = JLP, 

1140 
volume = 3, 

1141 
pages = {237258}, 

1142 
year = 1986, 

6619  1143 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82lcphigherorderresolution.dvi.gz}}} 
6592  1144 

1145 
@Article{paulsonsetI, 

1146 
author = {Lawrence C. Paulson}, 

1147 
title = {Set Theory for Verification: {I}. {From} 

1148 
Foundations to Functions}, 

1149 
journal = JAR, 

1150 
volume = 11, 

1151 
number = 3, 

1152 
pages = {353389}, 

1153 
year = 1993, 

14385  1154 
url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/setI.pdf}}} 
6592  1155 

1156 
@Article{paulsonsetII, 

1157 
author = {Lawrence C. Paulson}, 

1158 
title = {Set Theory for Verification: {II}. {Induction} and 

1159 
Recursion}, 

1160 
journal = JAR, 

1161 
volume = 15, 

1162 
number = 2, 

1163 
pages = {167215}, 

1164 
year = 1995, 

6619  1165 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz}}} 
6592  1166 

1167 
@article{paulson85, 

1168 
author = {Lawrence C. Paulson}, 

1169 
title = {Verifying the Unification Algorithm in {LCF}}, 

1170 
journal = SCP, 

1171 
volume = 5, 

1172 
pages = {143170}, 

1173 
year = 1985} 

1174 

11564  1175 
%replaces PaulsonLCF 
6592  1176 
@book{paulson87, 
1177 
author = {Lawrence C. Paulson}, 

1178 
title = {Logic and Computation: Interactive proof with Cambridge 

1179 
LCF}, 

1180 
year = 1987, 

1181 
publisher = CUP} 

1182 

1183 
@incollection{paulson700, 

1184 
author = {Lawrence C. Paulson}, 

1185 
title = {{Isabelle}: The Next 700 Theorem Provers}, 

1186 
crossref = {odifreddi90}, 

1187 
pages = {361386}, 

6619  1188 
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143lcpexperience.dvi.gz}}} 
6592  1189 

1190 
% replaces paulsonns and paulsonsecurity 

1191 
@Article{paulsonjcs, 

1192 
author = {Lawrence C. Paulson}, 

1193 
title = {The Inductive Approach to Verifying Cryptographic Protocols}, 

1194 
journal = JCS, 

1195 
year = 1998, 

1196 
volume = 6, 

1197 
pages = {85128}} 

1198 

11246  1199 
@Article{paulsontls, 
1200 
author = {Lawrence C. Paulson}, 

1201 
title = {Inductive Analysis of the {Internet} Protocol {TLS}}, 

1202 
journal = TISSEC, 

1203 
month = aug, 

1204 
year = 1999, 

1205 
volume = 2, 

1206 
number = 3, 

1207 
pages = {332351}} 

21074  1208 

1209 
@Article{paulsonyahalom, 

1210 
author = {Lawrence C. Paulson}, 

1211 
title = {Relations Between Secrets: 

1212 
Two Formal Analyses of the {Yahalom} Protocol}, 

1213 
journal = JCS, 

23505  1214 
volume = 9, 
1215 
number = 3, 

1216 
pages = {197216}, 

1217 
year = 2001}} 

11246  1218 

6592  1219 
@article{pelletier86, 
1220 
author = {F. J. Pelletier}, 

1221 
title = {Seventyfive Problems for Testing Automatic Theorem 

1222 
Provers}, 

1223 
journal = JAR, 

1224 
volume = 2, 

1225 
pages = {191216}, 

1226 
year = 1986, 

1227 
note = {Errata, JAR 4 (1988), 235236 and JAR 18 (1997), 135}} 

1228 

1229 
@Article{pitts94, 

1230 
author = {Andrew M. Pitts}, 

1231 
title = {A Coinduction Principle for Recursively Defined Domains}, 

1232 
journal = TCS, 

1233 
volume = 124, 

1234 
pages = {195219}, 

1235 
year = 1994} 

1236 

1237 
@Article{plaisted90, 

1238 
author = {David A. Plaisted}, 

1239 
title = {A SequentStyle Model Elimination Strategy and a Positive 

1240 
Refinement}, 

1241 
journal = JAR, 

1242 
year = 1990, 

1243 
volume = 6, 

1244 
number = 4, 

1245 
pages = {389402}} 

1246 

1247 
%Q 

1248 

1249 
@Article{quaife92, 

1250 
author = {Art Quaife}, 

1251 
title = {Automated Deduction in {von NeumannBernaysG\"{o}del} Set 

1252 
Theory}, 

1253 
journal = JAR, 

1254 
year = 1992, 

1255 
volume = 8, 

1256 
number = 1, 

1257 
pages = {91147}} 

1258 

1259 
%R 

1260 

1261 
@TechReport{rasmussen95, 

1262 
author = {Ole Rasmussen}, 

1263 
title = {The {ChurchRosser} Theorem in {Isabelle}: A Proof Porting 

1264 
Experiment}, 

1265 
institution = {Computer Laboratory, University of Cambridge}, 

1266 
year = 1995, 

1267 
number = 364, 

1268 
month = may, 

6619  1269 
url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364or200churchrosserisabelle.ps.gz}}} 
6592  1270 

1271 
@Book{reeves90, 

1272 
author = {Steve Reeves and Michael Clarke}, 

1273 
title = {Logic for Computer Science}, 

1274 
publisher = {AddisonWesley}, 

1275 
year = 1990} 

1276 

36926  1277 
@article{riazanovvoronkov2002, 
1278 
author = "Alexander Riazanov and Andrei Voronkov", 

1279 
title = "The Design and Implementation of {Vampire}", 

1280 
journal = "Journal of AI Communications", 

1281 
year = 2002, 

1282 
volume = 15, 

1283 
number ="2/3", 

1284 
pages = "91110"} 

1285 

11209  1286 
@book{RosenDMA,author={Kenneth H. Rosen}, 
1287 
title={Discrete Mathematics and Its Applications}, 

1288 
publisher={McGrawHill},year=1998} 

1289 

7041  1290 
@InProceedings{Rudnicki:1992:MizarOverview, 
1291 
author = {P. Rudnicki}, 

1292 
title = {An Overview of the {MIZAR} Project}, 

1293 
booktitle = {1992 Workshop on Types for Proofs and Programs}, 

1294 
year = 1992, 

1295 
organization = {Chalmers University of Technology}, 

1296 
publisher = {Bastad} 

1297 
} 

1298 

6592  1299 
%S 
1300 

1301 
@inproceedings{saaltinkfme, 

1302 
author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and 

1303 
Dan Craigen and Irwin Meisels}, 

1304 
title = {An {EVES} Data Abstraction Example}, 

1305 
pages = {578596}, 

1306 
crossref = {fme93}} 

1307 

29728  1308 
@Article{SchroederHeister:1984, 
1309 
author = {Peter SchroederHeister}, 

1310 
title = {A Natural Extension of Natural Deduction}, 

1311 
journal = {Journal of Symbolic Logic}, 

1312 
year = 1984, 

1313 
volume = 49, 

1314 
number = 4 

1315 
} 

1316 

36926  1317 
@article{schulz2002, 
1318 
author = "Stephan Schulz", 

1319 
title = "EA Brainiac Theorem Prover", 

1320 
journal = "Journal of AI Communications", 

1321 
year = 2002, 

1322 
volume = 15, 

1323 
number ="2/3", 

1324 
pages = "111126"} 

1325 

33191  1326 
@misc{sledgehammer2009, 
1327 
key = "Sledgehammer", 

1328 
title = "The {S}ledgehammer: Let Automatic Theorem Provers 

1329 
Write Your {I}s\a\belle Scripts", 

1330 
note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"} 

1331 

6592  1332 
@inproceedings{slindtfl, 
1333 
author = {Konrad Slind}, 

1334 
title = {Function Definition in Higher Order Logic}, 

23187  1335 
crossref = {tphols96}, 
1336 
pages = {381397}} 

6592  1337 

1338 
@book{suppes72, 

1339 
author = {Patrick Suppes}, 

1340 
title = {Axiomatic Set Theory}, 

1341 
year = 1972, 

1342 
publisher = {Dover}} 

1343 

36926  1344 
@inproceedings{sutcliffe2000, 
1345 
author = "Geoff Sutcliffe", 

1346 
title = "System Description: {SystemOnTPTP}", 

1347 
editor = "J. G. Carbonell and J. Siekmann", 

1348 
booktitle = {Automated Deduction  {CADE}17 International Conference}, 

1349 
series = "Lecture Notes in Artificial Intelligence", 

1350 
volume = {1831}, 

1351 
pages = "406410", 

1352 
year = 2000, 

1353 
publisher = Springer} 

1354 

6592  1355 
@InCollection{szasz93, 
1356 
author = {Nora Szasz}, 

1357 
title = {A Machine Checked Proof that {Ackermann's} Function is not 

1358 
Primitive Recursive}, 

1359 
crossref = {huetplotkin93}, 

1360 
pages = {317338}} 

1361 

7041  1362 
@TechReport{Syme:1997:DECLARE, 
1363 
author = {D. Syme}, 

1364 
title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic}, 

1365 
institution = {University of Cambridge Computer Laboratory}, 

1366 
year = 1997, 

1367 
number = 416 

1368 
} 

1369 

1370 
@PhdThesis{Syme:1998:thesis, 

1371 
author = {D. Syme}, 

1372 
title = {Declarative Theorem Proving for Operational Semantics}, 

1373 
school = {University of Cambridge}, 

1374 
year = 1998, 

1375 
note = {Submitted} 

1376 
} 

1377 

1378 
@InProceedings{Syme:1999:TPHOL, 

1379 
author = {D. Syme}, 

1380 
title = {Three Tactic Theorem Proving}, 

1381 
crossref = {tphols99}} 

1382 

6592  1383 
%T 
1384 

1385 
@book{takeuti87, 

1386 
author = {G. Takeuti}, 

1387 
title = {Proof Theory}, 

1388 
year = 1987, 

1389 
publisher = NH, 

1390 
edition = {2nd}} 

1391 

1392 
@Book{thompson91, 

1393 
author = {Simon Thompson}, 

1394 
title = {Type Theory and Functional Programming}, 

1395 
publisher = {AddisonWesley}, 

1396 
year = 1991} 

1397 

11209  1398 
@book{ThompsonHaskell,author={Simon Thompson}, 
1399 
title={Haskell: The Craft of Functional Programming}, 

1400 
publisher={AddisonWesley},year=1999} 

1401 

33191  1402 
@misc{kodkod2009, 
1403 
author = "Emina Torlak", 

1404 
title = {Kodkod: Constraint Solver for Relational Logic}, 

1405 
note = "\url{http://alloy.mit.edu/kodkod/}"} 

1406 

1407 
@misc{kodkod2009options, 

1408 
author = "Emina Torlak", 

1409 
title = "Kodkod {API}: Class {Options}", 

1410 
note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"} 

1411 

1412 
@inproceedings{torlakjackson2007, 

1413 
title = "Kodkod: A Relational Model Finder", 

1414 
author = "Emina Torlak and Daniel Jackson", 

1415 
editor = "Orna Grumberg and Michael Huth", 

1416 
booktitle = "TACAS 2007", 

1417 
series = LNCS, 

1418 
volume = {4424}, 

1419 
pages = "632647", 

1420 
year = 2007, 

1421 
publisher = Springer} 

1422 

7041  1423 
@Unpublished{Trybulec:1993:MizarFeatures, 
1424 
author = {A. Trybulec}, 

1425 
title = {Some Features of the {Mizar} Language}, 

1426 
note = {Presented at a workshop in Turin, Italy}, 

1427 
year = 1993 

1428 
} 

1429 

6592  1430 
%V 
1431 

1432 
@Unpublished{voelker94, 

10186  1433 
author = {Norbert V{\"o}lker}, 
6592  1434 
title = {The Verification of a Timer Program using {Isabelle/HOL}}, 
6745  1435 
url = {\url{ftp://ftp.fernunihagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}}, 
6592  1436 
year = 1994, 
1437 
month = aug} 

1438 

1439 
%W 

1440 

23956  1441 
@inproceedings{wadler89how, 
1442 
author = {P. Wadler and S. Blott}, 

1443 
title = {How to make adhoc polymorphism less adhoc}, 

1444 
booktitle = {ACM Symp.\ Principles of Programming Languages}, 

1445 
year = 1989 

1446 
} 

1447 

33191  1448 
@phdthesis{weber2008, 
1449 
author = "Tjark Weber", 

1450 
title = "SATBased Finite Model Generation for HigherOrder Logic", 

1451 
school = {Dept.\ of Informatics, T.U. M\"unchen}, 

1452 
type = "{Ph.D.}\ thesis", 

1453 
year = 2008} 

1454 

8505  1455 
@Misc{xsymbol, 
1456 
author = {Christoph Wedler}, 
