author | chaieb |
Sun, 08 Jul 2007 19:01:32 +0200 | |
changeset 23650 | 0a6a719d24d5 |
parent 14378 | 69c4d5997669 |
permissions | -rw-r--r-- |
7816 | 1 |
|
2 |
@string{CUCL="Comp. Lab., Univ. Camb."} |
|
3 |
@string{CUP="Cambridge University Press"} |
|
4 |
@string{Springer="Springer-Verlag"} |
|
5 |
@string{TUM="TU Munich"} |
|
6 |
||
8051 | 7 |
@Book{Concrete-Math, |
8 |
author = {R. L. Graham and D. E. Knuth and O. Patashnik}, |
|
9 |
title = {Concrete Mathematics}, |
|
10 |
publisher = {Addison-Wesley}, |
|
11 |
year = 1989 |
|
12 |
} |
|
13 |
||
10148 | 14 |
@InProceedings{Naraschewski-Wenzel:1998:HOOL, |
15 |
author = {Wolfgang Naraschewski and Markus Wenzel}, |
|
16 |
title = {Object-Oriented Verification based on Record Subtyping in |
|
17 |
{H}igher-{O}rder {L}ogic}, |
|
18 |
crossref = {tphols98}} |
|
19 |
||
20 |
@Article{Nipkow:1998:Winskel, |
|
21 |
author = {Tobias Nipkow}, |
|
22 |
title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, |
|
23 |
journal = {Formal Aspects of Computing}, |
|
24 |
year = 1998, |
|
25 |
volume = 10, |
|
26 |
pages = {171--186} |
|
27 |
} |
|
28 |
||
7968 | 29 |
@InProceedings{Wenzel:1999:TPHOL, |
30 |
author = {Markus Wenzel}, |
|
31 |
title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, |
|
32 |
crossref = {tphols99}} |
|
33 |
||
10148 | 34 |
@Book{Winskel:1993, |
35 |
author = {G. Winskel}, |
|
36 |
title = {The Formal Semantics of Programming Languages}, |
|
37 |
publisher = {MIT Press}, |
|
38 |
year = 1993 |
|
39 |
} |
|
40 |
||
7816 | 41 |
@Book{davey-priestley, |
42 |
author = {B. A. Davey and H. A. Priestley}, |
|
43 |
title = {Introduction to Lattices and Order}, |
|
44 |
publisher = CUP, |
|
45 |
year = 1990} |
|
46 |
||
47 |
@manual{isabelle-HOL, |
|
48 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, |
|
49 |
title = {{Isabelle}'s Logics: {HOL}}, |
|
50 |
institution = {Institut f\"ur Informatik, Technische Universi\"at |
|
51 |
M\"unchen and Computer Laboratory, University of Cambridge}} |
|
52 |
||
53 |
@manual{isabelle-intro, |
|
54 |
author = {Lawrence C. Paulson}, |
|
55 |
title = {Introduction to {Isabelle}}, |
|
56 |
institution = CUCL} |
|
57 |
||
58 |
@manual{isabelle-isar-ref, |
|
59 |
author = {Markus Wenzel}, |
|
7968 | 60 |
title = {The {Isabelle/Isar} Reference Manual}, |
7816 | 61 |
institution = TUM} |
62 |
||
7968 | 63 |
@manual{isabelle-ref, |
64 |
author = {Lawrence C. Paulson}, |
|
65 |
title = {The {Isabelle} Reference Manual}, |
|
66 |
institution = CUCL} |
|
67 |
||
68 |
@TechReport{paulson-mutilated-board, |
|
69 |
author = {Lawrence C. Paulson}, |
|
70 |
title = {A Simple Formalization and Proof for the Mutilated Chess Board}, |
|
71 |
institution = CUCL, |
|
72 |
year = 1996, |
|
73 |
number = 394, |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
10148
diff
changeset
|
74 |
note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}} |
7968 | 75 |
} |
7816 | 76 |
|
10148 | 77 |
@Proceedings{tphols98, |
78 |
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, |
|
79 |
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, |
|
80 |
editor = {Jim Grundy and Malcom Newey}, |
|
81 |
series = {LNCS}, |
|
82 |
volume = 1479, |
|
83 |
year = 1998} |
|
84 |
||
7816 | 85 |
@Proceedings{tphols99, |
86 |
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
|
87 |
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, |
|
88 |
editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and |
|
89 |
Paulin, C. and Thery, L.}, |
|
90 |
series = {LNCS 1690}, |
|
91 |
year = 1999} |