1 \begin{thebibliography}{10}
5 \newblock The lazy lambda calculus.
6 \newblock In David~A. Turner, editor, {\em Resesarch Topics in Functional
7 Programming}, pages 65--116. Addison-Wesley, 1977.
11 \newblock An introduction to inductive definitions.
12 \newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic}, pages
13 739--782. North-Holland, 1977.
17 \newblock {\em Non-Well-Founded Sets}.
21 Robert~S. Boyer and J~Strother Moore.
22 \newblock {\em A Computational Logic}.
23 \newblock Academic Press, 1979.
26 J.~Camilleri and T.~F. Melham.
27 \newblock Reasoning with inductively defined relations in the {HOL} theorem
29 \newblock Technical Report 265, University of Cambridge Computer Laboratory,
32 \bibitem{davey&priestley}
33 B.~A. Davey and H.~A. Priestley.
34 \newblock {\em Introduction to Lattices and Order}.
35 \newblock Cambridge University Press, 1990.
39 \newblock {\em The Semantics of Programming Languages: An Elementary
40 Introduction Using Structural Operational Semantics}.
41 \newblock Wiley, 1990.
45 \newblock Automating recursive type definitions in higher order logic.
46 \newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
47 Trends in Hardware Verification and Automated Theorem Proving}, pages
48 341--386. Springer, 1989.
52 \newblock {\em Communication and Concurrency}.
53 \newblock Prentice-Hall, 1989.
56 Christine Paulin-Mohring.
57 \newblock Inductive definitions in the system {Coq}: Rules and properties.
58 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
61 \bibitem{paulson-set-I}
63 \newblock Set theory for verification: {I}. {From} foundations to functions.
64 \newblock {\em Journal of Automated Reasoning}.
65 \newblock In press; draft available as Report 271, University of Cambridge
70 \newblock {\em {ML} for the Working Programmer}.
71 \newblock Cambridge University Press, 1991.
73 \bibitem{paulson-coind}
75 \newblock Co-induction and co-recursion in higher-order logic.
76 \newblock Technical Report 304, University of Cambridge Computer Laboratory,
79 \bibitem{isabelle-intro}
81 \newblock Introduction to {Isabelle}.
82 \newblock Technical Report 280, University of Cambridge Computer Laboratory,
85 \bibitem{paulson-set-II}
87 \newblock Set theory for verification: {II}. {Induction} and recursion.
88 \newblock Technical Report 312, University of Cambridge Computer Laboratory,
93 \newblock A co-induction principle for recursively defined domains.
94 \newblock {\em Theoretical Computer Science (Fundamental Studies)}.
95 \newblock In press; available as Report 252, University of Cambridge Computer
100 \newblock A machine checked proof that {Ackermann's} function is not primitive
102 \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
103 Environments}, pages 317--338. Cambridge University Press, 1993.
105 \end{thebibliography}