1 \begin{thebibliography}{10} |
1 \begin{thebibliography}{10} |
2 |
|
3 \bibitem{abrial93} |
|
4 J.~R. Abrial and G.~Laffitte. |
|
5 \newblock Towards the mechanization of the proofs of some classical theorems of |
|
6 set theory. |
|
7 \newblock preprint, February 1993. |
|
8 |
2 |
9 \bibitem{andrews86} |
3 \bibitem{andrews86} |
10 Peter~B. Andrews. |
4 Peter~B. Andrews. |
11 \newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth |
5 \newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth |
12 Through Proof}. |
6 Through Proof}. |
13 \newblock Academic Press, 1986. |
7 \newblock Academic Press, 1986. |
14 |
8 |
15 \bibitem{basin91} |
|
16 David Basin and Matt Kaufmann. |
|
17 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison. |
|
18 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical |
|
19 Frameworks}, pages 89--119. Cambridge University Press, 1991. |
|
20 |
|
21 \bibitem{boyer86} |
|
22 Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and |
|
23 Lawrence Wos. |
|
24 \newblock Set theory in first-order logic: Clauses for {G\"{o}del's} axioms. |
|
25 \newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986. |
|
26 |
|
27 \bibitem{camilleri92} |
|
28 J.~Camilleri and T.~F. Melham. |
|
29 \newblock Reasoning with inductively defined relations in the {HOL} theorem |
|
30 prover. |
|
31 \newblock Technical Report 265, Computer Laboratory, University of Cambridge, |
|
32 August 1992. |
|
33 |
|
34 \bibitem{church40} |
9 \bibitem{church40} |
35 Alonzo Church. |
10 Alonzo Church. |
36 \newblock A formulation of the simple theory of types. |
11 \newblock A formulation of the simple theory of types. |
37 \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. |
12 \newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940. |
38 |
13 |
45 \bibitem{constable86} |
20 \bibitem{constable86} |
46 R.~L. Constable et~al. |
21 R.~L. Constable et~al. |
47 \newblock {\em Implementing Mathematics with the Nuprl Proof Development |
22 \newblock {\em Implementing Mathematics with the Nuprl Proof Development |
48 System}. |
23 System}. |
49 \newblock Prentice-Hall, 1986. |
24 \newblock Prentice-Hall, 1986. |
50 |
|
51 \bibitem{davey&priestley} |
|
52 B.~A. Davey and H.~A. Priestley. |
|
53 \newblock {\em Introduction to Lattices and Order}. |
|
54 \newblock Cambridge University Press, 1990. |
|
55 |
|
56 \bibitem{devlin79} |
|
57 Keith~J. Devlin. |
|
58 \newblock {\em Fundamentals of Contemporary Set Theory}. |
|
59 \newblock Springer, 1979. |
|
60 |
|
61 \bibitem{dummett} |
|
62 Michael Dummett. |
|
63 \newblock {\em Elements of Intuitionism}. |
|
64 \newblock Oxford University Press, 1977. |
|
65 |
|
66 \bibitem{dyckhoff} |
|
67 Roy Dyckhoff. |
|
68 \newblock Contraction-free sequent calculi for intuitionistic logic. |
|
69 \newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992. |
|
70 |
25 |
71 \bibitem{felty91a} |
26 \bibitem{felty91a} |
72 Amy Felty. |
27 Amy Felty. |
73 \newblock A logic program for transforming sequent proofs to natural deduction |
28 \newblock A logic program for transforming sequent proofs to natural deduction |
74 proofs. |
29 proofs. |
91 M.~J.~C. Gordon and T.~F. Melham. |
46 M.~J.~C. Gordon and T.~F. Melham. |
92 \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher |
47 \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher |
93 Order Logic}. |
48 Order Logic}. |
94 \newblock Cambridge University Press, 1993. |
49 \newblock Cambridge University Press, 1993. |
95 |
50 |
96 \bibitem{halmos60} |
|
97 Paul~R. Halmos. |
|
98 \newblock {\em Naive Set Theory}. |
|
99 \newblock Van Nostrand, 1960. |
|
100 |
|
101 \bibitem{huet78} |
51 \bibitem{huet78} |
102 G.~P. Huet and B.~Lang. |
52 G.~P. Huet and B.~Lang. |
103 \newblock Proving and applying program transformations expressed with |
53 \newblock Proving and applying program transformations expressed with |
104 second-order patterns. |
54 second-order patterns. |
105 \newblock {\em Acta Informatica}, 11:31--55, 1978. |
55 \newblock {\em Acta Informatica}, 11:31--55, 1978. |
106 |
|
107 \bibitem{kunen80} |
|
108 Kenneth Kunen. |
|
109 \newblock {\em Set Theory: An Introduction to Independence Proofs}. |
|
110 \newblock North-Holland, 1980. |
|
111 |
56 |
112 \bibitem{alf} |
57 \bibitem{alf} |
113 Lena Magnusson and Bengt {Nordstr\"{o}m}. |
58 Lena Magnusson and Bengt {Nordstr\"{o}m}. |
114 \newblock The {ALF} proof editor and its proof engine. |
59 \newblock The {ALF} proof editor and its proof engine. |
115 \newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs |
60 \newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs |
138 |
83 |
139 \bibitem{Naraschewski-Wenzel:1998:TPHOL} |
84 \bibitem{Naraschewski-Wenzel:1998:TPHOL} |
140 Wolfgang Naraschewski and Markus Wenzel. |
85 Wolfgang Naraschewski and Markus Wenzel. |
141 \newblock Object-oriented verification based on record subtyping in |
86 \newblock Object-oriented verification based on record subtyping in |
142 higher-order logic. |
87 higher-order logic. |
143 \newblock In J.~Grundy and M.~Newey, editors, {\em Theorem Proving in Higher |
88 \newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in |
144 Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998. |
89 Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998. |
145 |
90 |
146 \bibitem{nazareth-nipkow} |
91 \bibitem{nazareth-nipkow} |
147 Dieter Nazareth and Tobias Nipkow. |
92 Dieter Nazareth and Tobias Nipkow. |
148 \newblock Formal verification of algorithm {W}: The monomorphic case. |
93 \newblock Formal verification of algorithm {W}: The monomorphic case. |
149 \newblock In von Wright et~al. \cite{tphols96}, pages 331--345. |
94 \newblock In von Wright et~al. \cite{tphols96}, pages 331--345. |
160 \newblock Winskel is (almost) right: Towards a mechanized semantics textbook. |
105 \newblock Winskel is (almost) right: Towards a mechanized semantics textbook. |
161 \newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software |
106 \newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software |
162 Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS}, |
107 Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS}, |
163 pages 180--192. Springer, 1996. |
108 pages 180--192. Springer, 1996. |
164 |
109 |
165 \bibitem{noel} |
|
166 Philippe No{\"e}l. |
|
167 \newblock Experimenting with {Isabelle} in {ZF} set theory. |
|
168 \newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993. |
|
169 |
|
170 \bibitem{nordstrom90} |
110 \bibitem{nordstrom90} |
171 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. |
111 Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith. |
172 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. |
112 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}. |
173 \newblock Oxford University Press, 1990. |
113 \newblock Oxford University Press, 1990. |
174 |
114 |
175 \bibitem{paulin92} |
|
176 Christine Paulin-Mohring. |
|
177 \newblock Inductive definitions in the system {Coq}: Rules and properties. |
|
178 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, |
|
179 December 1992. |
|
180 |
|
181 \bibitem{paulson85} |
115 \bibitem{paulson85} |
182 Lawrence~C. Paulson. |
116 Lawrence~C. Paulson. |
183 \newblock Verifying the unification algorithm in {LCF}. |
117 \newblock Verifying the unification algorithm in {LCF}. |
184 \newblock {\em Science of Computer Programming}, 5:143--170, 1985. |
118 \newblock {\em Science of Computer Programming}, 5:143--170, 1985. |
185 |
119 |
186 \bibitem{paulson87} |
120 \bibitem{paulson87} |
187 Lawrence~C. Paulson. |
121 Lawrence~C. Paulson. |
188 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
122 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. |
189 \newblock Cambridge University Press, 1987. |
123 \newblock Cambridge University Press, 1987. |
190 |
|
191 \bibitem{paulson-set-I} |
|
192 Lawrence~C. Paulson. |
|
193 \newblock Set theory for verification: {I}. {From} foundations to functions. |
|
194 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993. |
|
195 |
124 |
196 \bibitem{paulson-CADE} |
125 \bibitem{paulson-CADE} |
197 Lawrence~C. Paulson. |
126 Lawrence~C. Paulson. |
198 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
127 \newblock A fixedpoint approach to implementing (co)inductive definitions. |
199 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 |
128 \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 |
200 International Conference}, LNAI 814, pages 148--161. Springer, 1994. |
129 International Conference}, LNAI 814, pages 148--161. Springer, 1994. |
201 |
|
202 \bibitem{paulson-final} |
|
203 Lawrence~C. Paulson. |
|
204 \newblock A concrete final coalgebra theorem for {ZF} set theory. |
|
205 \newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em |
|
206 Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996, |
|
207 pages 120--139. Springer, 1995. |
|
208 |
130 |
209 \bibitem{paulson-set-II} |
131 \bibitem{paulson-set-II} |
210 Lawrence~C. Paulson. |
132 Lawrence~C. Paulson. |
211 \newblock Set theory for verification: {II}. {Induction} and recursion. |
133 \newblock Set theory for verification: {II}. {Induction} and recursion. |
212 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. |
134 \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. |
226 \bibitem{paulson-security} |
148 \bibitem{paulson-security} |
227 Lawrence~C. Paulson. |
149 Lawrence~C. Paulson. |
228 \newblock Proving properties of security protocols by induction. |
150 \newblock Proving properties of security protocols by induction. |
229 \newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83. |
151 \newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83. |
230 IEEE Computer Society Press, 1997. |
152 IEEE Computer Society Press, 1997. |
|
153 |
|
154 \bibitem{isabelle-ZF} |
|
155 Lawrence~C. Paulson. |
|
156 \newblock {Isabelle}'s logics: {FOL} and {ZF}. |
|
157 \newblock Technical report, Computer Laboratory, University of Cambridge, 1999. |
231 |
158 |
232 \bibitem{paulson-COLOG} |
159 \bibitem{paulson-COLOG} |
233 Lawrence~C. Paulson. |
160 Lawrence~C. Paulson. |
234 \newblock A formulation of the simple theory of types (for {Isabelle}). |
161 \newblock A formulation of the simple theory of types (for {Isabelle}). |
235 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
162 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88: |
245 \bibitem{plaisted90} |
172 \bibitem{plaisted90} |
246 David~A. Plaisted. |
173 David~A. Plaisted. |
247 \newblock A sequent-style model elimination strategy and a positive refinement. |
174 \newblock A sequent-style model elimination strategy and a positive refinement. |
248 \newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990. |
175 \newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990. |
249 |
176 |
250 \bibitem{quaife92} |
|
251 Art Quaife. |
|
252 \newblock Automated deduction in {von Neumann-Bernays-G\"{o}del} set theory. |
|
253 \newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992. |
|
254 |
|
255 \bibitem{slind-tfl} |
177 \bibitem{slind-tfl} |
256 Konrad Slind. |
178 Konrad Slind. |
257 \newblock Function definition in higher-order logic. |
179 \newblock Function definition in higher-order logic. |
258 \newblock In von Wright et~al. \cite{tphols96}. |
180 \newblock In von Wright et~al. \cite{tphols96}. |
259 |
181 |
260 \bibitem{suppes72} |
|
261 Patrick Suppes. |
|
262 \newblock {\em Axiomatic Set Theory}. |
|
263 \newblock Dover, 1972. |
|
264 |
|
265 \bibitem{takeuti87} |
182 \bibitem{takeuti87} |
266 G.~Takeuti. |
183 G.~Takeuti. |
267 \newblock {\em Proof Theory}. |
184 \newblock {\em Proof Theory}. |
268 \newblock North-Holland, 2nd edition, 1987. |
185 \newblock North-Holland, 2nd edition, 1987. |
269 |
186 |
275 \bibitem{tphols96} |
192 \bibitem{tphols96} |
276 J.~von Wright, J.~Grundy, and J.~Harrison, editors. |
193 J.~von Wright, J.~Grundy, and J.~Harrison, editors. |
277 \newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS |
194 \newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS |
278 1125, 1996. |
195 1125, 1996. |
279 |
196 |
280 \bibitem{principia} |
|
281 A.~N. Whitehead and B.~Russell. |
|
282 \newblock {\em Principia Mathematica}. |
|
283 \newblock Cambridge University Press, 1962. |
|
284 \newblock Paperback edition to *56, abridged from the 2nd edition (1927). |
|
285 |
|
286 \bibitem{winskel93} |
197 \bibitem{winskel93} |
287 Glynn Winskel. |
198 Glynn Winskel. |
288 \newblock {\em The Formal Semantics of Programming Languages}. |
199 \newblock {\em The Formal Semantics of Programming Languages}. |
289 \newblock MIT Press, 1993. |
200 \newblock MIT Press, 1993. |
290 |
201 |