1 \begin{thebibliography}{10}
5 \newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
7 \newblock Academic Press, 1986
10 Basin, D., Kaufmann, M.,
11 \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
12 \newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
13 Univ. Press, 1991, pp.~89--119
16 Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
17 \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
18 \newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
21 Boyer, R.~S., Moore, J.~S.,
22 \newblock {\em A Computational Logic Handbook},
23 \newblock Academic Press, 1988
26 Camilleri, J., Melham, T.~F.,
27 \newblock Reasoning with inductively defined relations in the {HOL} theorem
29 \newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
32 Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
33 \newblock {\em Artificial Intelligence Programming},
34 \newblock Lawrence Erlbaum Associates, 1980
38 \newblock A formulation of the simple theory of types,
39 \newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
43 \newblock {\em Interactive Program Derivation},
44 \newblock PhD thesis, University of Cambridge, 1992,
45 \newblock Computer Laboratory Technical Report 272
48 {Constable et al.}, R.~L.,
49 \newblock {\em Implementing Mathematics with the Nuprl Proof Development
51 \newblock Prentice-Hall, 1986
53 \bibitem{davey&priestley}
54 Davey, B.~A., Priestley, H.~A.,
55 \newblock {\em Introduction to Lattices and Order},
56 \newblock Cambridge Univ. Press, 1990
60 \newblock {\em A Generic Logic Environment},
61 \newblock PhD thesis, Imperial College, London, 1990
65 \newblock Lambda calculus notation with nameless dummies, a tool for automatic
66 formula manipulation, with application to the {Church-Rosser Theorem},
67 \newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
71 \newblock {\em Fundamentals of Contemporary Set Theory},
72 \newblock Springer, 1979
76 \newblock The {Coq} proof assistant user's guide,
77 \newblock Technical Report 134, INRIA-Rocquencourt, 1991
81 \newblock {\em Elements of Intuitionism},
82 \newblock Oxford University Press, 1977
86 \newblock Contraction-free sequent calculi for intuitionistic logic,
87 \newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
91 \newblock A logic program for transforming sequent proofs to natural deduction
93 \newblock In {\em Extensions of Logic Programming\/} (1991),
94 P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
99 \newblock Implementing tactics and tacticals in a higher-order logic
100 programming language,
101 \newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
105 \newblock A case study of co-induction in {Isabelle HOL},
106 \newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
109 Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
110 \newblock Principles of {OBJ2},
111 \newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
115 \newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
117 \newblock Harper \& Row, 1986
119 \bibitem{mgordon-hol}
120 Gordon, M. J.~C., Melham, T.~F.,
121 \newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
123 \newblock Cambridge Univ. Press, 1993
127 \newblock {\em Naive Set Theory},
128 \newblock Van Nostrand, 1960
130 \bibitem{harper-jacm}
131 Harper, R., Honsell, F., Plotkin, G.,
132 \newblock A framework for defining logics,
133 \newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
135 \bibitem{haskell-tutorial}
136 Hudak, P., Fasel, J.~H.,
137 \newblock A gentle introduction to {Haskell},
138 \newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
140 \bibitem{haskell-report}
141 Hudak, P., Jones, S.~P., Wadler, P.,
142 \newblock Report on the programming language {Haskell}: A non-strict, purely
144 \newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
145 \newblock Version 1.2
149 \newblock A unification algorithm for typed $\lambda$-calculus,
150 \newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
153 Huet, G.~P., Lang, B.,
154 \newblock Proving and applying program transformations expressed with
155 second-order patterns,
156 \newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
159 Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
160 \newblock {\em Mural: A Formal Development Support System},
161 \newblock Springer, 1991
164 Magnusson, L., {Nordstr\"om}, B.,
165 \newblock The {ALF} proof editor and its proof engine,
166 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
167 '93}\/} (published 1994), Springer, pp.~213--237,
171 Manna, Z., Waldinger, R.,
172 \newblock Deductive synthesis of the unification algorithm,
173 \newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
175 \bibitem{martin-nipkow}
176 Martin, U., Nipkow, T.,
177 \newblock Ordered rewriting and confluence,
178 \newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
179 Springer, pp.~366--380,
182 \bibitem{martinlof84}
184 \newblock {\em Intuitionistic type theory},
185 \newblock Bibliopolis, 1984
189 \newblock Automating recursive type definitions in higher order logic,
190 \newblock In {\em Current Trends in Hardware Verification and Automated Theorem
191 Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
194 \bibitem{miller-mixed}
196 \newblock Unification under a mixed prefix,
197 \newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
199 \bibitem{milner-coind}
200 Milner, R., Tofte, M.,
201 \newblock Co-induction in relational semantics,
202 \newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
204 \bibitem{nipkow-prehofer}
205 Nipkow, T., Prehofer, C.,
206 \newblock Type checking type classes,
207 \newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
208 \newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
212 \newblock Experimenting with {Isabelle} in {ZF} set theory,
213 \newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
215 \bibitem{nordstrom90}
216 {Nordstr\"om}, B., Petersson, K., Smith, J.,
217 \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
218 \newblock Oxford University Press, 1990
222 \newblock Inductive definitions in the system {Coq}: Rules and properties,
223 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
228 \newblock Verifying the unification algorithm in {LCF},
229 \newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
233 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
234 \newblock Cambridge Univ. Press, 1987
238 \newblock The foundation of a generic theorem prover,
239 \newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
241 \bibitem{paulson-COLOG}
243 \newblock A formulation of the simple theory of types (for {Isabelle}),
244 \newblock In {\em COLOG-88: International Conference on Computer Logic\/}
245 (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
251 \newblock {Isabelle}: The next 700 theorem provers,
252 \newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
253 Press, 1990, pp.~361--386
257 \newblock {\em {ML} for the Working Programmer},
258 \newblock Cambridge Univ. Press, 1991
260 \bibitem{paulson-coind}
262 \newblock Co-induction and co-recursion in higher-order logic,
263 \newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
265 \bibitem{paulson-fixedpt}
267 \newblock A fixedpoint approach to implementing (co)inductive definitions,
268 \newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
270 \bibitem{paulson-set-I}
272 \newblock Set theory for verification: {I}. {From} foundations to functions,
273 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
275 \bibitem{paulson-set-II}
277 \newblock Set theory for verification: {II}. {Induction} and recursion,
278 \newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
280 \bibitem{paulson-final}
282 \newblock A concrete final coalgebra theorem for {ZF} set theory,
283 \newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
285 \bibitem{pelletier86}
287 \newblock Seventy-five problems for testing automatic theorem provers,
288 \newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
289 \newblock Errata, JAR 4 (1988), 235--236
293 \newblock A sequent-style model elimination strategy and a positive refinement,
294 \newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
298 \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
299 \newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
302 Sawamura, H., Minami, T., Ohashi, K.,
303 \newblock Proof methods based on sheet of thought in {EUODHILOS},
304 \newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
305 Study of Social Information Science, Fujitsu Laboratories, 1992
309 \newblock {\em Axiomatic Set Theory},
310 \newblock Dover, 1972
314 \newblock {\em Proof Theory}, 2nd~ed.,
315 \newblock North Holland, 1987
319 \newblock {\em Type Theory and Functional Programming},
320 \newblock Addison-Wesley, 1991
323 Whitehead, A.~N., Russell, B.,
324 \newblock {\em Principia Mathematica},
325 \newblock Cambridge Univ. Press, 1962,
326 \newblock Paperback edition to *56, abridged from the 2nd edition (1927)
328 \bibitem{wos-bledsoe}
330 \newblock Automated reasoning and {Bledsoe's} dream for the field,
331 \newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
332 R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
334 \end{thebibliography}