|
1 % BibTeX database for the Isabelle documentation |
|
2 % |
|
3 % Lawrence C Paulson $Id$ |
|
4 |
|
5 %publishers |
|
6 @string{AP="Academic Press"} |
|
7 @string{CUP="Cambridge University Press"} |
|
8 @string{IEEE="{\sc ieee} Computer Society Press"} |
|
9 @string{LNCS="Lect.\ Notes in Comp.\ Sci."} |
|
10 @string{MIT="MIT Press"} |
|
11 @string{NH="North-Holland"} |
|
12 @string{Prentice="Prentice-Hall"} |
|
13 @string{Springer="Springer-Verlag"} |
|
14 |
|
15 %institutions |
|
16 @string{CUCL="Computer Laboratory, University of Cambridge"} |
|
17 |
|
18 %journals |
|
19 @string{FAC="Formal Aspects Comput."} |
|
20 @string{JAR="J. Auto. Reas."} |
|
21 @string{JCS="J. Comput. Secur."} |
|
22 @string{JFP="J. Func. Prog."} |
|
23 @string{JLC="J. Logic and Comput."} |
|
24 @string{JLP="J. Logic Prog."} |
|
25 @string{JSC="J. Symb. Comput."} |
|
26 @string{JSL="J. Symb. Logic"} |
|
27 @string{SIGPLAN="{SIGPLAN} Notices"} |
|
28 |
|
29 %conferences |
|
30 @string{CADE="International Conference on Automated Deduction"} |
|
31 @string{POPL="Symposium on Principles of Programming Languages"} |
|
32 @string{TYPES="Types for Proofs and Programs"} |
|
33 |
|
34 |
|
35 %A |
|
36 |
|
37 @incollection{abramsky90, |
|
38 author = {Samson Abramsky}, |
|
39 title = {The Lazy Lambda Calculus}, |
|
40 pages = {65-116}, |
|
41 editor = {David A. Turner}, |
|
42 booktitle = {Research Topics in Functional Programming}, |
|
43 publisher = {Addison-Wesley}, |
|
44 year = 1990} |
|
45 |
|
46 @Unpublished{abrial93, |
|
47 author = {J. R. Abrial and G. Laffitte}, |
|
48 title = {Towards the Mechanization of the Proofs of some Classical |
|
49 Theorems of Set Theory}, |
|
50 note = {preprint}, |
|
51 year = 1993, |
|
52 month = Feb} |
|
53 |
|
54 @incollection{aczel77, |
|
55 author = {Peter Aczel}, |
|
56 title = {An Introduction to Inductive Definitions}, |
|
57 pages = {739-782}, |
|
58 crossref = {barwise-handbk}} |
|
59 |
|
60 @Book{aczel88, |
|
61 author = {Peter Aczel}, |
|
62 title = {Non-Well-Founded Sets}, |
|
63 publisher = {CSLI}, |
|
64 year = 1988} |
|
65 |
|
66 @InProceedings{alf, |
|
67 author = {Lena Magnusson and Bengt {Nordstr\"{o}m}}, |
|
68 title = {The {ALF} Proof Editor and Its Proof Engine}, |
|
69 crossref = {types93}, |
|
70 pages = {213-237}} |
|
71 |
|
72 @book{andrews86, |
|
73 author = "Peter Andrews", |
|
74 title = "An Introduction to Mathematical Logic and Type Theory: to Truth |
|
75 through Proof", |
|
76 publisher = AP, |
|
77 series = "Computer Science and Applied Mathematics", |
|
78 year = 1986} |
|
79 |
|
80 %B |
|
81 |
|
82 @incollection{basin91, |
|
83 author = {David Basin and Matt Kaufmann}, |
|
84 title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental |
|
85 Comparison}, |
|
86 crossref = {huet-plotkin91}, |
|
87 pages = {89-119}} |
|
88 |
|
89 @Article{boyer86, |
|
90 author = {Robert Boyer and Ewing Lusk and William McCune and Ross |
|
91 Overbeek and Mark Stickel and Lawrence Wos}, |
|
92 title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's} |
|
93 Axioms}, |
|
94 journal = JAR, |
|
95 year = 1986, |
|
96 volume = 2, |
|
97 number = 3, |
|
98 pages = {287-327}} |
|
99 |
|
100 @book{bm79, |
|
101 author = {Robert S. Boyer and J Strother Moore}, |
|
102 title = {A Computational Logic}, |
|
103 publisher = {Academic Press}, |
|
104 year = 1979} |
|
105 |
|
106 @book{bm88book, |
|
107 author = {Robert S. Boyer and J Strother Moore}, |
|
108 title = {A Computational Logic Handbook}, |
|
109 publisher = {Academic Press}, |
|
110 year = 1988} |
|
111 |
|
112 @Article{debruijn72, |
|
113 author = {N. G. de Bruijn}, |
|
114 title = {Lambda Calculus Notation with Nameless Dummies, |
|
115 a Tool for Automatic Formula Manipulation, |
|
116 with Application to the {Church-Rosser Theorem}}, |
|
117 journal = {Indag. Math.}, |
|
118 volume = 34, |
|
119 pages = {381-392}, |
|
120 year = 1972} |
|
121 |
|
122 %C |
|
123 |
|
124 @TechReport{camilleri92, |
|
125 author = {J. Camilleri and T. F. Melham}, |
|
126 title = {Reasoning with Inductively Defined Relations in the |
|
127 {HOL} Theorem Prover}, |
|
128 institution = CUCL, |
|
129 year = 1992, |
|
130 number = 265, |
|
131 month = Aug} |
|
132 |
|
133 @Book{charniak80, |
|
134 author = {E. Charniak and C. K. Riesbeck and D. V. McDermott}, |
|
135 title = {Artificial Intelligence Programming}, |
|
136 publisher = {Lawrence Erlbaum Associates}, |
|
137 year = 1980} |
|
138 |
|
139 @article{church40, |
|
140 author = "Alonzo Church", |
|
141 title = "A Formulation of the Simple Theory of Types", |
|
142 journal = JSL, |
|
143 year = 1940, |
|
144 volume = 5, |
|
145 pages = "56-68"} |
|
146 |
|
147 @PhdThesis{coen92, |
|
148 author = {Martin D. Coen}, |
|
149 title = {Interactive Program Derivation}, |
|
150 school = {University of Cambridge}, |
|
151 note = {Computer Laboratory Technical Report 272}, |
|
152 month = nov, |
|
153 year = 1992} |
|
154 |
|
155 @book{constable86, |
|
156 author = {R. L. Constable and others}, |
|
157 title = {Implementing Mathematics with the Nuprl Proof |
|
158 Development System}, |
|
159 publisher = Prentice, |
|
160 year = 1986} |
|
161 |
|
162 %D |
|
163 |
|
164 @Book{davey&priestley, |
|
165 author = {B. A. Davey and H. A. Priestley}, |
|
166 title = {Introduction to Lattices and Order}, |
|
167 publisher = CUP, |
|
168 year = 1990} |
|
169 |
|
170 @Book{devlin79, |
|
171 author = {Keith J. Devlin}, |
|
172 title = {Fundamentals of Contemporary Set Theory}, |
|
173 publisher = {Springer}, |
|
174 year = 1979} |
|
175 |
|
176 @book{dummett, |
|
177 author = {Michael Dummett}, |
|
178 title = {Elements of Intuitionism}, |
|
179 year = 1977, |
|
180 publisher = {Oxford University Press}} |
|
181 |
|
182 @incollection{dybjer91, |
|
183 author = {Peter Dybjer}, |
|
184 title = {Inductive Sets and Families in {Martin-L\"of's} Type |
|
185 Theory and Their Set-Theoretic Semantics}, |
|
186 crossref = {huet-plotkin91}, |
|
187 pages = {280-306}} |
|
188 |
|
189 @Article{dyckhoff, |
|
190 author = {Roy Dyckhoff}, |
|
191 title = {Contraction-Free Sequent Calculi for Intuitionistic Logic}, |
|
192 journal = JSL, |
|
193 year = 1992, |
|
194 volume = 57, |
|
195 number = 3, |
|
196 pages = {795-807}} |
|
197 |
|
198 %F |
|
199 |
|
200 @InProceedings{felty91a, |
|
201 Author = {Amy Felty}, |
|
202 Title = {A Logic Program for Transforming Sequent Proofs to Natural |
|
203 Deduction Proofs}, |
|
204 crossref = {extensions91}, |
|
205 pages = {157-178}} |
|
206 |
|
207 @TechReport{frost93, |
|
208 author = {Jacob Frost}, |
|
209 title = {A Case Study of Co-induction in {Isabelle HOL}}, |
|
210 institution = CUCL, |
|
211 number = 308, |
|
212 year = 1993, |
|
213 month = Aug} |
|
214 |
|
215 %revised version of frost93 |
|
216 @TechReport{frost95, |
|
217 author = {Jacob Frost}, |
|
218 title = {A Case Study of Co-induction in {Isabelle}}, |
|
219 institution = CUCL, |
|
220 number = 359, |
|
221 year = 1995, |
|
222 month = Feb} |
|
223 |
|
224 @inproceedings{OBJ, |
|
225 author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud |
|
226 and J. Meseguer}, |
|
227 title = {Principles of {OBJ2}}, |
|
228 booktitle = POPL, |
|
229 year = 1985, |
|
230 pages = {52-66}} |
|
231 |
|
232 %G |
|
233 |
|
234 @book{gallier86, |
|
235 author = {J. H. Gallier}, |
|
236 title = {Logic for Computer Science: |
|
237 Foundations of Automatic Theorem Proving}, |
|
238 year = 1986, |
|
239 publisher = {Harper \& Row}} |
|
240 |
|
241 @Book{galton90, |
|
242 author = {Antony Galton}, |
|
243 title = {Logic for Information Technology}, |
|
244 publisher = {Wiley}, |
|
245 year = 1990} |
|
246 |
|
247 @InProceedings{gimenez-codifying, |
|
248 author = {Eduardo Gim{\'e}nez}, |
|
249 title = {Codifying Guarded Definitions with Recursive Schemes}, |
|
250 crossref = {types94}, |
|
251 pages = {39-59} |
|
252 } |
|
253 |
|
254 @Book{mgordon-hol, |
|
255 author = {M. J. C. Gordon and T. F. Melham}, |
|
256 title = {Introduction to {HOL}: A Theorem Proving Environment for |
|
257 Higher Order Logic}, |
|
258 publisher = CUP, |
|
259 year = 1993} |
|
260 |
|
261 @book{mgordon79, |
|
262 author = {Michael J. C. Gordon and Robin Milner and Christopher P. |
|
263 Wadsworth}, |
|
264 title = {Edinburgh {LCF}: A Mechanised Logic of Computation}, |
|
265 year = 1979, |
|
266 publisher = {Springer}, |
|
267 series = {LNCS 78}} |
|
268 |
|
269 @InProceedings{gunter-trees, |
|
270 author = {Elsa L. Gunter}, |
|
271 title = {A Broader Class of Trees for Recursive Type Definitions for |
|
272 {HOL}}, |
|
273 crossref = {hug93}, |
|
274 pages = {141-154}} |
|
275 |
|
276 %H |
|
277 |
|
278 @Book{halmos60, |
|
279 author = {Paul R. Halmos}, |
|
280 title = {Naive Set Theory}, |
|
281 publisher = {Van Nostrand}, |
|
282 year = 1960} |
|
283 |
|
284 @Book{hennessy90, |
|
285 author = {Matthew Hennessy}, |
|
286 title = {The Semantics of Programming Languages: An Elementary |
|
287 Introduction Using Structural Operational Semantics}, |
|
288 publisher = {Wiley}, |
|
289 year = 1990} |
|
290 |
|
291 @Article{haskell-report, |
|
292 author = {Paul Hudak and Simon Peyton Jones and Philip Wadler}, |
|
293 title = {Report on the Programming Language {Haskell}: A |
|
294 Non-strict, Purely Functional Language}, |
|
295 journal = SIGPLAN, |
|
296 year = 1992, |
|
297 volume = 27, |
|
298 number = 5, |
|
299 month = May, |
|
300 note = {Version 1.2}} |
|
301 |
|
302 @Article{haskell-tutorial, |
|
303 author = {Paul Hudak and Joseph H. Fasel}, |
|
304 title = {A Gentle Introduction to {Haskell}}, |
|
305 journal = SIGPLAN, |
|
306 year = 1992, |
|
307 volume = 27, |
|
308 number = 5, |
|
309 month = May} |
|
310 |
|
311 @article{huet75, |
|
312 author = {G. P. Huet}, |
|
313 title = {A Unification Algorithm for Typed $\lambda$-Calculus}, |
|
314 journal = TCS, |
|
315 volume = 1, |
|
316 year = 1975, |
|
317 pages = {27-57}} |
|
318 |
|
319 @article{huet78, |
|
320 author = {G. P. Huet and B. Lang}, |
|
321 title = {Proving and Applying Program Transformations Expressed with |
|
322 Second-Order Patterns}, |
|
323 journal = acta, |
|
324 volume = 11, |
|
325 year = 1978, |
|
326 pages = {31-55}} |
|
327 |
|
328 @inproceedings{huet88, |
|
329 author = {G\'erard Huet}, |
|
330 title = {Induction Principles Formalized in the {Calculus of |
|
331 Constructions}}, |
|
332 booktitle = {Programming of Future Generation Computers}, |
|
333 editor = {K. Fuchi and M. Nivat}, |
|
334 year = 1988, |
|
335 pages = {205-216}, |
|
336 publisher = {Elsevier}} |
|
337 |
|
338 %K |
|
339 |
|
340 @Book{kunen80, |
|
341 author = {Kenneth Kunen}, |
|
342 title = {Set Theory: An Introduction to Independence Proofs}, |
|
343 publisher = NH, |
|
344 year = 1980} |
|
345 |
|
346 %M |
|
347 |
|
348 @Article{mw81, |
|
349 author = {Zohar Manna and Richard Waldinger}, |
|
350 title = {Deductive Synthesis of the Unification Algorithm}, |
|
351 journal = SCP, |
|
352 year = 1981, |
|
353 volume = 1, |
|
354 number = 1, |
|
355 pages = {5-48}} |
|
356 |
|
357 @InProceedings{martin-nipkow, |
|
358 author = {Ursula Martin and Tobias Nipkow}, |
|
359 title = {Ordered Rewriting and Confluence}, |
|
360 crossref = {cade10}, |
|
361 pages = {366-380}} |
|
362 |
|
363 @book{martinlof84, |
|
364 author = {Per Martin-L\"of}, |
|
365 title = {Intuitionistic type theory}, |
|
366 year = 1984, |
|
367 publisher = {Bibliopolis}} |
|
368 |
|
369 @incollection{melham89, |
|
370 author = {Thomas F. Melham}, |
|
371 title = {Automating Recursive Type Definitions in Higher Order |
|
372 Logic}, |
|
373 pages = {341-386}, |
|
374 crossref = {birtwistle89}} |
|
375 |
|
376 @Article{miller-mixed, |
|
377 Author = {Dale Miller}, |
|
378 Title = {Unification Under a Mixed Prefix}, |
|
379 journal = JSC, |
|
380 volume = 14, |
|
381 number = 4, |
|
382 pages = {321-358}, |
|
383 Year = 1992} |
|
384 |
|
385 @Article{milner78, |
|
386 author = {Robin Milner}, |
|
387 title = {A Theory of Type Polymorphism in Programming}, |
|
388 journal = "J. Comp.\ Sys.\ Sci.", |
|
389 year = 1978, |
|
390 volume = 17, |
|
391 pages = {348-375}} |
|
392 |
|
393 @TechReport{milner-ind, |
|
394 author = {Robin Milner}, |
|
395 title = {How to Derive Inductions in {LCF}}, |
|
396 institution = Edinburgh, |
|
397 year = 1980, |
|
398 type = {note}} |
|
399 |
|
400 @Article{milner-coind, |
|
401 author = {Robin Milner and Mads Tofte}, |
|
402 title = {Co-induction in Relational Semantics}, |
|
403 journal = TCS, |
|
404 year = 1991, |
|
405 volume = 87, |
|
406 pages = {209-220}} |
|
407 |
|
408 @Book{milner89, |
|
409 author = {Robin Milner}, |
|
410 title = {Communication and Concurrency}, |
|
411 publisher = Prentice, |
|
412 year = 1989} |
|
413 |
|
414 @PhdThesis{monahan84, |
|
415 author = {Brian Q. Monahan}, |
|
416 title = {Data Type Proofs using Edinburgh {LCF}}, |
|
417 school = {University of Edinburgh}, |
|
418 year = 1984} |
|
419 |
|
420 %N |
|
421 |
|
422 @InProceedings{NaraschewskiW-TPHOLs98, |
|
423 author = {Wolfgang Naraschewski and Markus Wenzel}, |
|
424 title = |
|
425 {Object-Oriented Verification based on Record Subtyping in Higher-Order Logic}, |
|
426 booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'98)}, |
|
427 publisher = Springer, |
|
428 volume = 1479, |
|
429 series = LNCS, |
|
430 year = 1998} |
|
431 |
|
432 @inproceedings{nazareth-nipkow, |
|
433 author = {Dieter Nazareth and Tobias Nipkow}, |
|
434 title = {Formal Verification of Algorithm {W}: The Monomorphic Case}, |
|
435 crossref = {tphols96}, |
|
436 pages = {331-345}, |
|
437 year = 1996} |
|
438 |
|
439 @inproceedings{nipkow-W, |
|
440 author = {Wolfgang Naraschewski and Tobias Nipkow}, |
|
441 title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}}, |
|
442 booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96}, |
|
443 editor = {E. Gim\'enez and C. Paulin-Mohring}, |
|
444 publisher = Springer, |
|
445 series = LNCS, |
|
446 volume = 1512, |
|
447 pages = {317-332}, |
|
448 year = 1998} |
|
449 |
|
450 @inproceedings{Nipkow-CR, |
|
451 author = {Tobias Nipkow}, |
|
452 title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, |
|
453 booktitle = {Automated Deduction --- CADE-13}, |
|
454 editor = {M. McRobbie and J.K. Slaney}, |
|
455 publisher = Springer, |
|
456 series = LNCS, |
|
457 volume = 1104, |
|
458 pages = {733-747}, |
|
459 year = 1996} |
|
460 |
|
461 % WAS Nipkow-LICS-93 |
|
462 @InProceedings{nipkow-patterns, |
|
463 title = {Functional Unification of Higher-Order Patterns}, |
|
464 author = {Tobias Nipkow}, |
|
465 pages = {64-74}, |
|
466 crossref = {lics8}, |
|
467 url = {ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}, |
|
468 keywords = {unification}} |
|
469 |
|
470 @article{nipkow-IMP, |
|
471 author = {Tobias Nipkow}, |
|
472 title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, |
|
473 journal = FAC, |
|
474 volume = 10, |
|
475 pages = {171-186}, |
|
476 year = 1998} |
|
477 |
|
478 @article{nipkow-prehofer, |
|
479 author = {Tobias Nipkow and Christian Prehofer}, |
|
480 title = {Type Reconstruction for Type Classes}, |
|
481 journal = JFP, |
|
482 volume = 5, |
|
483 number = 2, |
|
484 year = 1995, |
|
485 pages = {201-224}} |
|
486 |
|
487 @Article{noel, |
|
488 author = {Philippe No{\"e}l}, |
|
489 title = {Experimenting with {Isabelle} in {ZF} Set Theory}, |
|
490 journal = JAR, |
|
491 volume = 10, |
|
492 number = 1, |
|
493 pages = {15-58}, |
|
494 year = 1993} |
|
495 |
|
496 @book{nordstrom90, |
|
497 author = {Bengt {Nordstr\"om} and Kent Petersson and Jan Smith}, |
|
498 title = {Programming in {Martin-L\"of}'s Type Theory. An |
|
499 Introduction}, |
|
500 publisher = {Oxford University Press}, |
|
501 year = 1990} |
|
502 |
|
503 %O |
|
504 |
|
505 @Manual{pvs-language, |
|
506 title = {The {PVS} specification language}, |
|
507 author = {S. Owre and N. Shankar and J. M. Rushby}, |
|
508 organization = {Computer Science Laboratory, SRI International}, |
|
509 address = {Menlo Park, CA}, |
|
510 note = {Beta release}, |
|
511 year = 1993, |
|
512 month = apr, |
|
513 url = {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}} |
|
514 |
|
515 %P |
|
516 |
|
517 % replaces paulin92 |
|
518 @InProceedings{paulin-tlca, |
|
519 author = {Christine Paulin-Mohring}, |
|
520 title = {Inductive Definitions in the System {Coq}: Rules and |
|
521 Properties}, |
|
522 crossref = {tlca93}, |
|
523 pages = {328-345}} |
|
524 |
|
525 @InProceedings{paulson-CADE, |
|
526 author = {Lawrence C. Paulson}, |
|
527 title = {A Fixedpoint Approach to Implementing (Co)Inductive |
|
528 Definitions}, |
|
529 pages = {148-161}, |
|
530 crossref = {cade12}} |
|
531 |
|
532 @InProceedings{paulson-COLOG, |
|
533 author = {Lawrence C. Paulson}, |
|
534 title = {A Formulation of the Simple Theory of Types (for |
|
535 {Isabelle})}, |
|
536 pages = {246-274}, |
|
537 crossref = {colog88}, |
|
538 url = {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}} |
|
539 |
|
540 @Article{paulson-coind, |
|
541 author = {Lawrence C. Paulson}, |
|
542 title = {Mechanizing Coinduction and Corecursion in Higher-Order |
|
543 Logic}, |
|
544 journal = JLC, |
|
545 year = 1997, |
|
546 volume = 7, |
|
547 number = 2, |
|
548 month = mar, |
|
549 pages = {175-204}} |
|
550 |
|
551 @techreport{isabelle-ZF, |
|
552 author = {Lawrence C. Paulson}, |
|
553 title = {{Isabelle}'s Logics: {FOL} and {ZF}}, |
|
554 institution = CUCL, |
|
555 year = 1999} |
|
556 |
|
557 @article{paulson-found, |
|
558 author = {Lawrence C. Paulson}, |
|
559 title = {The Foundation of a Generic Theorem Prover}, |
|
560 journal = JAR, |
|
561 volume = 5, |
|
562 number = 3, |
|
563 pages = {363-397}, |
|
564 year = 1989, |
|
565 url = {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}} |
|
566 |
|
567 %replaces paulson-final |
|
568 @Article{paulson-mscs, |
|
569 author = {Lawrence C. Paulson}, |
|
570 title = {Final Coalgebras as Greatest Fixed Points in ZF Set Theory}, |
|
571 journal = {Mathematical Structures in Computer Science}, |
|
572 year = 1999, |
|
573 volume = 9, |
|
574 note = {in press}} |
|
575 |
|
576 @InCollection{paulson-generic, |
|
577 author = {Lawrence C. Paulson}, |
|
578 title = {Generic Automatic Proof Tools}, |
|
579 crossref = {wos-fest}, |
|
580 chapter = 3} |
|
581 |
|
582 @Article{paulson-gr, |
|
583 author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski}, |
|
584 title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of |
|
585 Choice}, |
|
586 journal = JAR, |
|
587 year = 1996, |
|
588 volume = 17, |
|
589 number = 3, |
|
590 month = dec, |
|
591 pages = {291-323}} |
|
592 |
|
593 @InCollection{paulson-handbook, |
|
594 author = {Lawrence C. Paulson}, |
|
595 title = {Designing a Theorem Prover}, |
|
596 crossref = {handbk-lics2}, |
|
597 pages = {415-475}} |
|
598 |
|
599 @Book{paulson-isa-book, |
|
600 author = {Lawrence C. Paulson}, |
|
601 title = {Isabelle: A Generic Theorem Prover}, |
|
602 publisher = {Springer}, |
|
603 year = 1994, |
|
604 note = {LNCS 828}} |
|
605 |
|
606 @InCollection{paulson-markt, |
|
607 author = {Lawrence C. Paulson}, |
|
608 title = {Tool Support for Logics of Programs}, |
|
609 booktitle = {Mathematical Methods in Program Development: |
|
610 Summer School Marktoberdorf 1996}, |
|
611 publisher = {Springer}, |
|
612 pages = {461-498}, |
|
613 year = {Published 1997}, |
|
614 editor = {Manfred Broy}, |
|
615 series = {NATO ASI Series F}} |
|
616 |
|
617 %replaces Paulson-ML and paulson91 |
|
618 @book{paulson-ml2, |
|
619 author = {Lawrence C. Paulson}, |
|
620 title = {{ML} for the Working Programmer}, |
|
621 year = 1996, |
|
622 edition = {2nd}, |
|
623 publisher = CUP} |
|
624 |
|
625 @article{paulson-natural, |
|
626 author = {Lawrence C. Paulson}, |
|
627 title = {Natural Deduction as Higher-order Resolution}, |
|
628 journal = JLP, |
|
629 volume = 3, |
|
630 pages = {237-258}, |
|
631 year = 1986, |
|
632 url = {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}} |
|
633 |
|
634 @Article{paulson-set-I, |
|
635 author = {Lawrence C. Paulson}, |
|
636 title = {Set Theory for Verification: {I}. {From} |
|
637 Foundations to Functions}, |
|
638 journal = JAR, |
|
639 volume = 11, |
|
640 number = 3, |
|
641 pages = {353-389}, |
|
642 year = 1993, |
|
643 url = {ftp://ftp.cl.cam.ac.uk/ml/set-I.ps.gz}} |
|
644 |
|
645 @Article{paulson-set-II, |
|
646 author = {Lawrence C. Paulson}, |
|
647 title = {Set Theory for Verification: {II}. {Induction} and |
|
648 Recursion}, |
|
649 journal = JAR, |
|
650 volume = 15, |
|
651 number = 2, |
|
652 pages = {167-215}, |
|
653 year = 1995, |
|
654 url = {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}} |
|
655 |
|
656 @article{paulson85, |
|
657 author = {Lawrence C. Paulson}, |
|
658 title = {Verifying the Unification Algorithm in {LCF}}, |
|
659 journal = SCP, |
|
660 volume = 5, |
|
661 pages = {143-170}, |
|
662 year = 1985} |
|
663 |
|
664 %replqces Paulson-LCF |
|
665 @book{paulson87, |
|
666 author = {Lawrence C. Paulson}, |
|
667 title = {Logic and Computation: Interactive proof with Cambridge |
|
668 LCF}, |
|
669 year = 1987, |
|
670 publisher = CUP} |
|
671 |
|
672 @incollection{paulson700, |
|
673 author = {Lawrence C. Paulson}, |
|
674 title = {{Isabelle}: The Next 700 Theorem Provers}, |
|
675 crossref = {odifreddi90}, |
|
676 pages = {361-386}, |
|
677 url = {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}} |
|
678 |
|
679 % replaces paulson-ns and paulson-security |
|
680 @Article{paulson-jcs, |
|
681 author = {Lawrence C. Paulson}, |
|
682 title = {The Inductive Approach to Verifying Cryptographic Protocols}, |
|
683 journal = JCS, |
|
684 year = 1998, |
|
685 volume = 6, |
|
686 pages = {85-128}} |
|
687 |
|
688 @article{pelletier86, |
|
689 author = {F. J. Pelletier}, |
|
690 title = {Seventy-five Problems for Testing Automatic Theorem |
|
691 Provers}, |
|
692 journal = JAR, |
|
693 volume = 2, |
|
694 pages = {191-216}, |
|
695 year = 1986, |
|
696 note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}} |
|
697 |
|
698 @Article{pitts94, |
|
699 author = {Andrew M. Pitts}, |
|
700 title = {A Co-induction Principle for Recursively Defined Domains}, |
|
701 journal = TCS, |
|
702 volume = 124, |
|
703 pages = {195-219}, |
|
704 year = 1994} |
|
705 |
|
706 @Article{plaisted90, |
|
707 author = {David A. Plaisted}, |
|
708 title = {A Sequent-Style Model Elimination Strategy and a Positive |
|
709 Refinement}, |
|
710 journal = JAR, |
|
711 year = 1990, |
|
712 volume = 6, |
|
713 number = 4, |
|
714 pages = {389-402}} |
|
715 |
|
716 %Q |
|
717 |
|
718 @Article{quaife92, |
|
719 author = {Art Quaife}, |
|
720 title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set |
|
721 Theory}, |
|
722 journal = JAR, |
|
723 year = 1992, |
|
724 volume = 8, |
|
725 number = 1, |
|
726 pages = {91-147}} |
|
727 |
|
728 %R |
|
729 |
|
730 @TechReport{rasmussen95, |
|
731 author = {Ole Rasmussen}, |
|
732 title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting |
|
733 Experiment}, |
|
734 institution = {Computer Laboratory, University of Cambridge}, |
|
735 year = 1995, |
|
736 number = 364, |
|
737 month = may, |
|
738 url = {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}} |
|
739 |
|
740 @Book{reeves90, |
|
741 author = {Steve Reeves and Michael Clarke}, |
|
742 title = {Logic for Computer Science}, |
|
743 publisher = {Addison-Wesley}, |
|
744 year = 1990} |
|
745 |
|
746 %S |
|
747 |
|
748 @inproceedings{saaltink-fme, |
|
749 author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and |
|
750 Dan Craigen and Irwin Meisels}, |
|
751 title = {An {EVES} Data Abstraction Example}, |
|
752 pages = {578-596}, |
|
753 crossref = {fme93}} |
|
754 |
|
755 @inproceedings{slind-tfl, |
|
756 author = {Konrad Slind}, |
|
757 title = {Function Definition in Higher Order Logic}, |
|
758 booktitle = {Theorem Proving in Higher Order Logics}, |
|
759 editor = {J. von Wright and J. Grundy and J. Harrison}, |
|
760 publisher = Springer, |
|
761 series = LNCS, |
|
762 volume = 1125, |
|
763 pages = {381-397}, |
|
764 year = 1996} |
|
765 |
|
766 @book{suppes72, |
|
767 author = {Patrick Suppes}, |
|
768 title = {Axiomatic Set Theory}, |
|
769 year = 1972, |
|
770 publisher = {Dover}} |
|
771 |
|
772 @InCollection{szasz93, |
|
773 author = {Nora Szasz}, |
|
774 title = {A Machine Checked Proof that {Ackermann's} Function is not |
|
775 Primitive Recursive}, |
|
776 crossref = {huet-plotkin93}, |
|
777 pages = {317-338}} |
|
778 |
|
779 %T |
|
780 |
|
781 @book{takeuti87, |
|
782 author = {G. Takeuti}, |
|
783 title = {Proof Theory}, |
|
784 year = 1987, |
|
785 publisher = NH, |
|
786 edition = {2nd}} |
|
787 |
|
788 @Book{thompson91, |
|
789 author = {Simon Thompson}, |
|
790 title = {Type Theory and Functional Programming}, |
|
791 publisher = {Addison-Wesley}, |
|
792 year = 1991} |
|
793 |
|
794 %V |
|
795 |
|
796 @Unpublished{voelker94, |
|
797 author = {Norbert V\"olker}, |
|
798 title = {The Verification of a Timer Program using {Isabelle/HOL}}, |
|
799 url = {ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}, |
|
800 year = 1994, |
|
801 month = aug} |
|
802 |
|
803 %W |
|
804 |
|
805 @book{principia, |
|
806 author = {A. N. Whitehead and B. Russell}, |
|
807 title = {Principia Mathematica}, |
|
808 year = 1962, |
|
809 publisher = CUP, |
|
810 note = {Paperback edition to *56, |
|
811 abridged from the 2nd edition (1927)}} |
|
812 |
|
813 @book{winskel93, |
|
814 author = {Glynn Winskel}, |
|
815 title = {The Formal Semantics of Programming Languages}, |
|
816 publisher = MIT,year=1993} |
|
817 |
|
818 @InCollection{wos-bledsoe, |
|
819 author = {Larry Wos}, |
|
820 title = {Automated Reasoning and {Bledsoe's} Dream for the Field}, |
|
821 crossref = {bledsoe-fest}, |
|
822 pages = {297-342}} |
|
823 |
|
824 |
|
825 % CROSS REFERENCES |
|
826 |
|
827 @book{handbk-lics2, |
|
828 editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum}, |
|
829 title = {Handbook of Logic in Computer Science}, |
|
830 booktitle = {Handbook of Logic in Computer Science}, |
|
831 publisher = {Oxford University Press}, |
|
832 year = 1992, |
|
833 volume = 2} |
|
834 |
|
835 @book{types93, |
|
836 editor = {Henk Barendregt and Tobias Nipkow}, |
|
837 title = TYPES # {: International Workshop {TYPES '93}}, |
|
838 booktitle = TYPES # {: International Workshop {TYPES '93}}, |
|
839 year = {published 1994}, |
|
840 publisher = {Springer}, |
|
841 series = {LNCS 806}} |
|
842 |
|
843 @Proceedings{tlca93, |
|
844 title = {Typed Lambda Calculi and Applications}, |
|
845 booktitle = {Typed Lambda Calculi and Applications}, |
|
846 editor = {M. Bezem and J.F. Groote}, |
|
847 year = 1993, |
|
848 publisher = {Springer}, |
|
849 series = {LNCS 664}} |
|
850 |
|
851 @book{bledsoe-fest, |
|
852 title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, |
|
853 booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, |
|
854 publisher = {Kluwer Academic Publishers}, |
|
855 year = 1991, |
|
856 editor = {Robert S. Boyer}} |
|
857 |
|
858 @Proceedings{cade12, |
|
859 editor = {Alan Bundy}, |
|
860 title = {Automated Deduction --- {CADE}-12 |
|
861 International Conference}, |
|
862 booktitle = {Automated Deduction --- {CADE}-12 |
|
863 International Conference}, |
|
864 year = 1994, |
|
865 series = {LNAI 814}, |
|
866 publisher = {Springer}} |
|
867 |
|
868 @book{types94, |
|
869 editor = {Peter Dybjer and Bengt Nordstr{\"om} and Jan Smith}, |
|
870 title = TYPES # {: International Workshop {TYPES '94}}, |
|
871 booktitle = TYPES # {: International Workshop {TYPES '94}}, |
|
872 year = 1995, |
|
873 publisher = {Springer}, |
|
874 series = {LNCS 996}} |
|
875 |
|
876 @book{huet-plotkin91, |
|
877 editor = {{G\'erard} Huet and Gordon Plotkin}, |
|
878 title = {Logical Frameworks}, |
|
879 booktitle = {Logical Frameworks}, |
|
880 publisher = CUP, |
|
881 year = 1991} |
|
882 |
|
883 @proceedings{colog88, |
|
884 editor = {P. Martin-L\"of and G. Mints}, |
|
885 title = {COLOG-88: International Conference on Computer Logic}, |
|
886 booktitle = {COLOG-88: International Conference on Computer Logic}, |
|
887 year = {Published 1990}, |
|
888 publisher = {Springer}, |
|
889 organization = {Estonian Academy of Sciences}, |
|
890 address = {Tallinn}, |
|
891 series = {LNCS 417}} |
|
892 |
|
893 @book{odifreddi90, |
|
894 editor = {P. Odifreddi}, |
|
895 title = {Logic and Computer Science}, |
|
896 booktitle = {Logic and Computer Science}, |
|
897 publisher = {Academic Press}, |
|
898 year = 1990} |
|
899 |
|
900 @proceedings{extensions91, |
|
901 editor = {Peter Schroeder-Heister}, |
|
902 title = {Extensions of Logic Programming}, |
|
903 booktitle = {Extensions of Logic Programming}, |
|
904 year = 1991, |
|
905 series = {LNAI 475}, |
|
906 publisher = {Springer}} |
|
907 |
|
908 @proceedings{cade10, |
|
909 editor = {Mark E. Stickel}, |
|
910 title = {10th } # CADE, |
|
911 booktitle = {10th } # CADE, |
|
912 year = 1990, |
|
913 publisher = {Springer}, |
|
914 series = {LNAI 449}} |
|
915 |
|
916 @Proceedings{lics8, |
|
917 editor = {M. Vardi}, |
|
918 title = {Eighth Annual Symposium on Logic in Computer Science}, |
|
919 booktitle = {Eighth Annual Symposium on Logic in Computer Science}, |
|
920 publisher = IEEE, |
|
921 year = 1993} |
|
922 |
|
923 @book{wos-fest, |
|
924 title = {Automated Reasoning and its Applications: |
|
925 Essays in Honor of {Larry Wos}}, |
|
926 booktitle = {Automated Reasoning and its Applications: |
|
927 Essays in Honor of {Larry Wos}}, |
|
928 publisher = {MIT Press}, |
|
929 year = 1997, |
|
930 editor = {Robert Veroff}} |
|
931 |
|
932 @Proceedings{tphols96, |
|
933 title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, |
|
934 booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96}, |
|
935 editor = {J. von Wright and J. Grundy and J. Harrison}, |
|
936 series = {LNCS 1125}, |
|
937 year = 1996} |