doc-src/Inductive/ind-defs.bbl

HOL/Update

\begin{thebibliography}{10}

\bibitem{abramsky90}
Abramsky, S.,
\newblock The lazy lambda calculus,
\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
  Addison-Wesley, 1977, pp.~65--116

\bibitem{aczel77}
Aczel, P.,
\newblock An introduction to inductive definitions,
\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
  North-Holland, 1977, pp.~739--782

\bibitem{aczel88}
Aczel, P.,
\newblock {\em Non-Well-Founded Sets},
\newblock CSLI, 1988

\bibitem{bm79}
Boyer, R.~S., Moore, J.~S.,
\newblock {\em A Computational Logic},
\newblock Academic Press, 1979

\bibitem{camilleri92}
Camilleri, J., Melham, T.~F.,
\newblock Reasoning with inductively defined relations in the {HOL} theorem
  prover,
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992

\bibitem{davey&priestley}
Davey, B.~A., Priestley, H.~A.,
\newblock {\em Introduction to Lattices and Order},
\newblock Cambridge Univ. Press, 1990

\bibitem{dybjer91}
Dybjer, P.,
\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
  set-theoretic semantics,
\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ.
  Press, 1991, pp.~280--306

\bibitem{types94}
Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
\newblock {\em Types for Proofs and Programs: International Workshop {TYPES
  '94}},
\newblock LNCS 996. Springer, published 1995

\bibitem{IMPS}
Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
\newblock {IMPS}: An interactive mathematical proof system,
\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248

\bibitem{frost95}
Frost, J.,
\newblock A case study of co-induction in {Isabelle},
\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995

\bibitem{gimenez-codifying}
Gim{\'e}nez, E.,
\newblock Codifying guarded definitions with recursive schemes,
\newblock In Dybjer et~al. \cite{types94}, pp.~39--59

\bibitem{gunter-trees}
Gunter, E.~L.,
\newblock A broader class of trees for recursive type definitions for {HOL},
\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG
  '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,
  pp.~141--154

\bibitem{hennessy90}
Hennessy, M.,
\newblock {\em The Semantics of Programming Languages: An Elementary
  Introduction Using Structural Operational Semantics},
\newblock Wiley, 1990

\bibitem{huet88}
Huet, G.,
\newblock Induction principles formalized in the {Calculus of Constructions},
\newblock In {\em Programming of Future Generation Computers\/} (1988),
  K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216

\bibitem{melham89}
Melham, T.~F.,
\newblock Automating recursive type definitions in higher order logic,
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
  Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386

\bibitem{milner-ind}
Milner, R.,
\newblock How to derive inductions in {LCF},
\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980

\bibitem{milner89}
Milner, R.,
\newblock {\em Communication and Concurrency},
\newblock Prentice-Hall, 1989

\bibitem{milner-coind}
Milner, R., Tofte, M.,
\newblock Co-induction in relational semantics,
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220

\bibitem{monahan84}
Monahan, B.~Q.,
\newblock {\em Data Type Proofs using Edinburgh {LCF}},
\newblock PhD thesis, University of Edinburgh, 1984

\bibitem{nipkow-CR}
Nipkow, T.,
\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/}
  (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747

\bibitem{pvs-language}
Owre, S., Shankar, N., Rushby, J.~M.,
\newblock {\em The {PVS} specification language},
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.
  1993,
\newblock Beta release

\bibitem{paulin-tlca}
Paulin-Mohring, C.,
\newblock Inductive definitions in the system {Coq}: Rules and properties,
\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
  J.~Groote, Eds., LNCS 664, Springer, pp.~328--345

\bibitem{paulson87}
Paulson, L.~C.,
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
\newblock Cambridge Univ. Press, 1987

\bibitem{paulson-set-I}
Paulson, L.~C.,
\newblock Set theory for verification: {I}. {From} foundations to functions,
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389

\bibitem{paulson-isa-book}
Paulson, L.~C.,
\newblock {\em Isabelle: A Generic Theorem Prover},
\newblock Springer, 1994,
\newblock LNCS 828

\bibitem{paulson-set-II}
Paulson, L.~C.,
\newblock Set theory for verification: {II}. {Induction} and recursion,
\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215

\bibitem{paulson-coind}
Paulson, L.~C.,
\newblock Mechanizing coinduction and corecursion in higher-order logic,
\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204

\bibitem{paulson-final}
Paulson, L.~C.,
\newblock A concrete final coalgebra theorem for {ZF} set theory,
\newblock In Dybjer et~al. \cite{types94}, pp.~120--139

\bibitem{paulson-markt}
Paulson, L.~C.,
\newblock Tool support for logics of programs,
\newblock In {\em Mathematical Methods in Program Development: Summer School
  Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published
  1997, pp.~461--498

\bibitem{paulson-gr}
Paulson, L.~C., Gr\c{a}bczewski, K.,
\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323

\bibitem{pitts94}
Pitts, A.~M.,
\newblock A co-induction principle for recursively defined domains,
\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219

\bibitem{rasmussen95}
Rasmussen, O.,
\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
  experiment,
\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
  1995

\bibitem{saaltink-fme}
Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
\newblock An {EVES} data abstraction example,
\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
  J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596

\bibitem{slind-tfl}
Slind, K.,
\newblock Function definition in higher-order logic,
\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
  (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125

\bibitem{szasz93}
Szasz, N.,
\newblock A machine checked proof that {Ackermann's} function is not primitive
  recursive,
\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
  Univ. Press, 1993, pp.~317--338

\bibitem{voelker95}
V\"olker, N.,
\newblock On the representation of datatypes in {Isabelle/HOL},
\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
  1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
  pp.~206--218

\bibitem{winskel93}
Winskel, G.,
\newblock {\em The Formal Semantics of Programming Languages},
\newblock MIT Press, 1993

\end{thebibliography}