doc-src/ind-defs.bbl
author clasohm
Tue, 09 May 1995 10:42:23 +0200
changeset 1112 737a1a0df754
parent 606 d5b322b33afb
child 1184 94ada3b54caa
permissions -rw-r--r--
added \CHOL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
\begin{thebibliography}{10}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\bibitem{abramsky90}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
     4
Abramsky, S.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
     5
\newblock The lazy lambda calculus,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
     6
\newblock In {\em Resesarch Topics in Functional Programming}, D.~A. Turner,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
     7
  Ed. Addison-Wesley, 1977, pp.~65--116
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
\bibitem{aczel77}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    10
Aczel, P.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    11
\newblock An introduction to inductive definitions,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    12
\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    13
  North-Holland, 1977, pp.~739--782
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\bibitem{aczel88}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    16
Aczel, P.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    17
\newblock {\em Non-Well-Founded Sets},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    18
\newblock CSLI, 1988
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\bibitem{bm79}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    21
Boyer, R.~S., Moore, J.~S.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    22
\newblock {\em A Computational Logic},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    23
\newblock Academic Press, 1979
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
\bibitem{camilleri92}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    26
Camilleri, J., Melham, T.~F.,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
\newblock Reasoning with inductively defined relations in the {HOL} theorem
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    28
  prover,
606
d5b322b33afb minor updates
lcp
parents: 293
diff changeset
    29
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\bibitem{davey&priestley}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    32
Davey, B.~A., Priestley, H.~A.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    33
\newblock {\em Introduction to Lattices and Order},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    34
\newblock Cambridge Univ. Press, 1990
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    35
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    36
\bibitem{dybjer91}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    37
Dybjer, P.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    38
\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    39
  set-theoretic semantics,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    40
\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    41
  Univ. Press, 1991, pp.~280--306
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    42
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    43
\bibitem{IMPS}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    44
Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    45
\newblock {IMPS}: An interactive mathematical proof system,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    46
\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
\bibitem{hennessy90}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    49
Hennessy, M.,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
\newblock {\em The Semantics of Programming Languages: An Elementary
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    51
  Introduction Using Structural Operational Semantics},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    52
\newblock Wiley, 1990
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    53
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    54
\bibitem{huet88}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    55
Huet, G.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    56
\newblock Induction principles formalized in the {Calculus of Constructions},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    57
\newblock In {\em Programming of Future Generation Computers\/} (1988),
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    58
  Elsevier, pp.~205--216
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\bibitem{melham89}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    61
Melham, T.~F.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    62
\newblock Automating recursive type definitions in higher order logic,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    63
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    64
  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    65
  pp.~341--386
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    66
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    67
\bibitem{milner-ind}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    68
Milner, R.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    69
\newblock How to derive inductions in {LCF},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    70
\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
\bibitem{milner89}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    73
Milner, R.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    74
\newblock {\em Communication and Concurrency},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    75
\newblock Prentice-Hall, 1989
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    76
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    77
\bibitem{monahan84}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    78
Monahan, B.~Q.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    79
\newblock {\em Data Type Proofs using Edinburgh {LCF}},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    80
\newblock PhD thesis, University of Edinburgh, 1984
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\bibitem{paulin92}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    83
Paulin-Mohring, C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    84
\newblock Inductive definitions in the system {Coq}: Rules and properties,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    85
\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    86
  1992
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    88
\bibitem{paulson87}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    89
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    90
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    91
\newblock Cambridge Univ. Press, 1987
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\bibitem{paulson91}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    94
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    95
\newblock {\em {ML} for the Working Programmer},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    96
\newblock Cambridge Univ. Press, 1991
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\bibitem{paulson-coind}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
    99
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   100
\newblock Co-induction and co-recursion in higher-order logic,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   101
\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
\bibitem{isabelle-intro}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   104
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   105
\newblock Introduction to {Isabelle},
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   106
\newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   107
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   108
\bibitem{paulson-set-I}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   109
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   110
\newblock Set theory for verification: {I}. {From} foundations to functions,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   111
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\bibitem{paulson-set-II}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   114
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   115
\newblock Set theory for verification: {II}. {Induction} and recursion,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   116
\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   117
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   118
\bibitem{paulson-final}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   119
Paulson, L.~C.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   120
\newblock A concrete final coalgebra theorem for {ZF} set theory,
606
d5b322b33afb minor updates
lcp
parents: 293
diff changeset
   121
\newblock Tech. Rep. 334, Comp. Lab., Univ. Cambridge, 1994
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
\bibitem{pitts94}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   124
Pitts, A.~M.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   125
\newblock A co-induction principle for recursively defined domains,
606
d5b322b33afb minor updates
lcp
parents: 293
diff changeset
   126
\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   127
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   128
\bibitem{saaltink-fme}
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   129
Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   130
\newblock An {EVES} data abstraction example,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   131
\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   132
  J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   133
\newblock LNCS 670
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
\bibitem{szasz93}
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   136
Szasz, N.,
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\newblock A machine checked proof that {Ackermann's} function is not primitive
293
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   138
  recursive,
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   139
\newblock In {\em Logical Environments}, G.~Huet, G.~Plotkin, Eds. Cambridge
63a0077dd9f2 first draft of Springer volume
lcp
parents: 104
diff changeset
   140
  Univ. Press, 1993, pp.~317--338
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\end{thebibliography}