104

1 
\begin{thebibliography}{10}


2 


3 
\bibitem{abramsky90}


4 
Samson Abramsky.


5 
\newblock The lazy lambda calculus.


6 
\newblock In David~A. Turner, editor, {\em Resesarch Topics in Functional


7 
Programming}, pages 65116. AddisonWesley, 1977.


8 


9 
\bibitem{aczel77}


10 
Peter Aczel.


11 
\newblock An introduction to inductive definitions.


12 
\newblock In J.~Barwise, editor, {\em Handbook of Mathematical Logic}, pages


13 
739782. NorthHolland, 1977.


14 


15 
\bibitem{aczel88}


16 
Peter Aczel.


17 
\newblock {\em NonWellFounded Sets}.


18 
\newblock CSLI, 1988.


19 


20 
\bibitem{bm79}


21 
Robert~S. Boyer and J~Strother Moore.


22 
\newblock {\em A Computational Logic}.


23 
\newblock Academic Press, 1979.


24 


25 
\bibitem{camilleri92}


26 
J.~Camilleri and T.~F. Melham.


27 
\newblock Reasoning with inductively defined relations in the {HOL} theorem


28 
prover.


29 
\newblock Technical Report 265, University of Cambridge Computer Laboratory,


30 
August 1992.


31 


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.


36 


37 
\bibitem{hennessy90}


38 
Matthew Hennessy.


39 
\newblock {\em The Semantics of Programming Languages: An Elementary


40 
Introduction Using Structural Operational Semantics}.


41 
\newblock Wiley, 1990.


42 


43 
\bibitem{melham89}


44 
Thomas~F. Melham.


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 
341386. Springer, 1989.


49 


50 
\bibitem{milner89}


51 
Robin Milner.


52 
\newblock {\em Communication and Concurrency}.


53 
\newblock PrenticeHall, 1989.


54 


55 
\bibitem{paulin92}


56 
Christine PaulinMohring.


57 
\newblock Inductive definitions in the system {Coq}: Rules and properties.


58 
\newblock Research Report 9249, LIP, Ecole Normale Sup\'erieure de Lyon,


59 
December 1992.


60 


61 
\bibitem{paulsonsetI}


62 
Lawrence~C. Paulson.


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


66 
Computer Laboratory.


67 


68 
\bibitem{paulson91}


69 
Lawrence~C. Paulson.


70 
\newblock {\em {ML} for the Working Programmer}.


71 
\newblock Cambridge University Press, 1991.


72 


73 
\bibitem{paulsoncoind}


74 
Lawrence~C. Paulson.


75 
\newblock Coinduction and corecursion in higherorder logic.


76 
\newblock Technical Report 304, University of Cambridge Computer Laboratory,


77 
July 1993.


78 


79 
\bibitem{isabelleintro}


80 
Lawrence~C. Paulson.


81 
\newblock Introduction to {Isabelle}.


82 
\newblock Technical Report 280, University of Cambridge Computer Laboratory,


83 
1993.


84 


85 
\bibitem{paulsonsetII}


86 
Lawrence~C. Paulson.


87 
\newblock Set theory for verification: {II}. {Induction} and recursion.


88 
\newblock Technical Report 312, University of Cambridge Computer Laboratory,


89 
1993.


90 


91 
\bibitem{pitts94}


92 
Andrew~M. Pitts.


93 
\newblock A coinduction 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


96 
Laboratory.


97 


98 
\bibitem{szasz93}


99 
Nora Szasz.


100 
\newblock A machine checked proof that {Ackermann's} function is not primitive


101 
recursive.


102 
\newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical


103 
Environments}, pages 317338. Cambridge University Press, 1993.


104 


105 
\end{thebibliography}
