14569
|
1 |
@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
|
|
2 |
title={Compiling Exceptions Correctly},
|
|
3 |
booktitle={Proc.\ Conf.\ Mathematics of Program Construction},
|
|
4 |
year=2004,note={To appear}}
|
|
5 |
|
12101
|
6 |
@InProceedings{Kamm-et-al:1999,
|
|
7 |
author = {Florian Kamm{\"u}ller and Markus Wenzel and
|
|
8 |
Lawrence C. Paulson},
|
|
9 |
title = {Locales: A Sectioning Concept for {Isabelle}},
|
|
10 |
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
|
|
11 |
editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
|
|
12 |
Paulin, C. and Thery, L.},
|
|
13 |
series = {LNCS},
|
|
14 |
volume = 1690,
|
|
15 |
year = 1999}
|
|
16 |
|
|
17 |
@InProceedings{Naraschewski-Wenzel:1998,
|
|
18 |
author = {Wolfgang Naraschewski and Markus Wenzel},
|
|
19 |
title = {Object-Oriented Verification based on Record Subtyping in
|
|
20 |
{H}igher-{O}rder {L}ogic},
|
|
21 |
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
|
|
22 |
editor = {Jim Grundy and Malcom Newey},
|
|
23 |
series = {LNCS},
|
|
24 |
volume = 1479,
|
|
25 |
year = 1998}
|
|
26 |
|
|
27 |
@Manual{Nipkow-et-al:2001:HOL,
|
|
28 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
|
29 |
title = {{Isabelle}'s Logics: {HOL}},
|
|
30 |
institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
|
|
31 |
M{\"u}nchen and Computer Laboratory, University of Cambridge},
|
|
32 |
year = 2001,
|
|
33 |
note = {Part of the Isabelle distribution,
|
|
34 |
\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
|
|
35 |
}
|
|
36 |
|
12900
|
37 |
@Article{Paulson:1989,
|
|
38 |
author = {L. C. Paulson},
|
|
39 |
title = {The foundation of a generic Theorem Prover},
|
|
40 |
journal = {Journal of Automated Reasoning},
|
|
41 |
year = 1989,
|
|
42 |
volume = 5,
|
|
43 |
number = 3,
|
|
44 |
pages = {363--397}
|
|
45 |
}
|
|
46 |
|
13446
|
47 |
@Book{Paulson:1994:Isabelle,
|
|
48 |
author = {L. C. Paulson and T. Nipkow},
|
|
49 |
title = {{Isabelle}: A Generic Theorem Prover},
|
|
50 |
year = 1994,
|
|
51 |
series = {LNCS},
|
|
52 |
volume = {828},
|
|
53 |
publisher = {Springer}
|
|
54 |
}
|
|
55 |
|
12101
|
56 |
@InProceedings{Wenzel:1999,
|
|
57 |
author = {Markus Wenzel},
|
|
58 |
title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
|
|
59 |
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
|
|
60 |
editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
|
|
61 |
Paulin, C. and Thery, L.},
|
|
62 |
series = {LNCS},
|
|
63 |
volume = 1690,
|
|
64 |
year = 1999}
|
|
65 |
|
12508
|
66 |
@Unpublished{Wenzel:2001:Isar-examples,
|
|
67 |
author = {Markus Wenzel},
|
|
68 |
title = {Miscellaneous {I}sabelle/{I}sar examples for
|
|
69 |
Higher-Order Logic},
|
|
70 |
year = 2001,
|
|
71 |
note = {Part of the Isabelle distribution,
|
33026
|
72 |
\url{http://isabelle.in.tum.de/library/HOL/Isar_Examples/document.pdf}}
|
12508
|
73 |
}
|
13446
|
74 |
|
12101
|
75 |
@PhdThesis{Wenzel:2001:Thesis,
|
|
76 |
author = {Markus Wenzel},
|
|
77 |
title = {Isabelle/Isar --- a versatile environment for human-readable
|
|
78 |
formal proof documents},
|
|
79 |
school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
|
|
80 |
year = 2001,
|
|
81 |
month = {September},
|
|
82 |
note = {Submitted}
|
|
83 |
}
|
|
84 |
@Manual{Wenzel:2001:isar-ref,
|
|
85 |
author = {Markus Wenzel},
|
|
86 |
title = {The {Isabelle/Isar} Reference Manual},
|
|
87 |
year = 2001,
|
|
88 |
institution = {TU M{\"u}nchen},
|
|
89 |
note = {Part of the Isabelle distribution,
|
|
90 |
\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
|
|
91 |
}
|
13446
|
92 |
|
|
93 |
@Book{isabelle-hol-book,
|
|
94 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
|
95 |
title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
|
|
96 |
publisher = {Springer},
|
|
97 |
year = 2002,
|
|
98 |
note = {LNCS 2283}}
|
15871
|
99 |
|
|
100 |
@Misc{McMillan-LectureNotes,
|
|
101 |
author = {Ken McMillan},
|
|
102 |
title = {Lecture notes on verification of digital and hybrid systems},
|
|
103 |
note = {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
|
|
104 |
}
|
|
105 |
|
|
106 |
@PhdThesis{McMillan-PhDThesis,
|
|
107 |
author = {Ken McMillan},
|
|
108 |
title = {Symbolic Model Checking: an approach to the state explosion problem},
|
|
109 |
school = {Carnegie Mellon University},
|
|
110 |
year = 1992
|
|
111 |
} |