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 |
|
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 |
|
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 |
|
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 |
|
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 |
|
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, |
|
72 \url{http://isabelle.in.tum.de/library/HOL/Isar_Examples/document.pdf}} |
|
73 } |
|
74 |
|
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 } |
|
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}} |
|
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 } |
|