doc-src/Inductive/ind-defs.bbl
author wenzelm
Sun, 29 Nov 1998 13:16:47 +0100
changeset 5989 9670dae0143d
parent 4985 aaaf64da9e3a
permissions -rw-r--r--
proof_general_trans (experimental);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     1
\begin{thebibliography}{10}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     2
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     3
\bibitem{abramsky90}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     4
Abramsky, S.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     5
\newblock The lazy lambda calculus,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     6
\newblock In {\em Research Topics in Functional Programming}, D.~A. Turner, Ed.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     7
  Addison-Wesley, 1977, pp.~65--116
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     8
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
     9
\bibitem{aczel77}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    10
Aczel, P.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    11
\newblock An introduction to inductive definitions,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    12
\newblock In {\em Handbook of Mathematical Logic}, J.~Barwise, Ed.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    13
  North-Holland, 1977, pp.~739--782
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    14
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    15
\bibitem{aczel88}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    16
Aczel, P.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    17
\newblock {\em Non-Well-Founded Sets},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    18
\newblock CSLI, 1988
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    19
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    20
\bibitem{bm79}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    21
Boyer, R.~S., Moore, J.~S.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    22
\newblock {\em A Computational Logic},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    23
\newblock Academic Press, 1979
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    24
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    25
\bibitem{camilleri92}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    26
Camilleri, J., Melham, T.~F.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    27
\newblock Reasoning with inductively defined relations in the {HOL} theorem
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    28
  prover,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    29
\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    30
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    31
\bibitem{davey&priestley}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    32
Davey, B.~A., Priestley, H.~A.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    33
\newblock {\em Introduction to Lattices and Order},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    34
\newblock Cambridge Univ. Press, 1990
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    35
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    36
\bibitem{dybjer91}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    37
Dybjer, P.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    38
\newblock Inductive sets and families in {Martin-L\"of's} type theory and their
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    39
  set-theoretic semantics,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    40
\newblock In {\em Logical Frameworks}, G.~Huet G.~Plotkin, Eds. Cambridge Univ.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    41
  Press, 1991, pp.~280--306
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    42
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    43
\bibitem{types94}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    44
Dybjer, P., Nordstr{\"om}, B., Smith, J., Eds.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    45
\newblock {\em Types for Proofs and Programs: International Workshop {TYPES
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    46
  '94}},
4985
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
    47
\newblock LNCS 996. Springer, 1995
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    48
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    49
\bibitem{IMPS}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    50
Farmer, W.~M., Guttman, J.~D., Thayer, F.~J.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    51
\newblock {IMPS}: An interactive mathematical proof system,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    52
\newblock {\em J. Auto. Reas. {\bf 11}}, 2 (1993), 213--248
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    53
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    54
\bibitem{frost95}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    55
Frost, J.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    56
\newblock A case study of co-induction in {Isabelle},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    57
\newblock Tech. Rep. 359, Comp. Lab., Univ. Cambridge, Feb. 1995
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    58
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    59
\bibitem{gimenez-codifying}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    60
Gim{\'e}nez, E.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    61
\newblock Codifying guarded definitions with recursive schemes,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    62
\newblock In Dybjer et~al. \cite{types94}, pp.~39--59
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    63
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    64
\bibitem{gunter-trees}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    65
Gunter, E.~L.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    66
\newblock A broader class of trees for recursive type definitions for {HOL},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    67
\newblock In {\em Higher Order Logic Theorem Proving and Its Applications: HUG
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    68
  '93\/} (Published 1994), J.~Joyce C.~Seger, Eds., LNCS 780, Springer,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    69
  pp.~141--154
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    70
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    71
\bibitem{hennessy90}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    72
Hennessy, M.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    73
\newblock {\em The Semantics of Programming Languages: An Elementary
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    74
  Introduction Using Structural Operational Semantics},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    75
\newblock Wiley, 1990
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    76
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    77
\bibitem{huet88}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    78
Huet, G.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    79
\newblock Induction principles formalized in the {Calculus of Constructions},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    80
\newblock In {\em Programming of Future Generation Computers\/} (1988),
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    81
  K.~Fuchi M.~Nivat, Eds., Elsevier, pp.~205--216
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    82
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    83
\bibitem{melham89}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    84
Melham, T.~F.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    85
\newblock Automating recursive type definitions in higher order logic,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    86
\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    87
  Proving}, G.~Birtwistle P.~A. Subrahmanyam, Eds. Springer, 1989, pp.~341--386
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    88
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    89
\bibitem{milner-ind}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    90
Milner, R.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    91
\newblock How to derive inductions in {LCF},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    92
\newblock note, Dept. Comp. Sci., Univ. Edinburgh, 1980
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    93
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    94
\bibitem{milner89}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    95
Milner, R.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    96
\newblock {\em Communication and Concurrency},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    97
\newblock Prentice-Hall, 1989
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    98
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
    99
\bibitem{milner-coind}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   100
Milner, R., Tofte, M.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   101
\newblock Co-induction in relational semantics,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   102
\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   103
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   104
\bibitem{monahan84}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   105
Monahan, B.~Q.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   106
\newblock {\em Data Type Proofs using Edinburgh {LCF}},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   107
\newblock PhD thesis, University of Edinburgh, 1984
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   108
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   109
\bibitem{nipkow-CR}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   110
Nipkow, T.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   111
\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}),
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   112
\newblock In {\em Automated Deduction --- {CADE}-13 International Conference\/}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   113
  (1996), M.~McRobbie J.~K. Slaney, Eds., LNAI 1104, Springer, pp.~733--747
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   114
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   115
\bibitem{pvs-language}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   116
Owre, S., Shankar, N., Rushby, J.~M.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   117
\newblock {\em The {PVS} specification language},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   118
\newblock Computer Science Laboratory, SRI International, Menlo Park, CA, Apr.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   119
  1993,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   120
\newblock Beta release
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   121
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   122
\bibitem{paulin-tlca}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   123
Paulin-Mohring, C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   124
\newblock Inductive definitions in the system {Coq}: Rules and properties,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   125
\newblock In {\em Typed Lambda Calculi and Applications\/} (1993), M.~Bezem
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   126
  J.~Groote, Eds., LNCS 664, Springer, pp.~328--345
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   127
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   128
\bibitem{paulson87}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   129
Paulson, L.~C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   130
\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   131
\newblock Cambridge Univ. Press, 1987
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   132
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   133
\bibitem{paulson-set-I}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   134
Paulson, L.~C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   135
\newblock Set theory for verification: {I}. {From} foundations to functions,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   136
\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   137
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   138
\bibitem{paulson-isa-book}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   139
Paulson, L.~C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   140
\newblock {\em Isabelle: A Generic Theorem Prover},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   141
\newblock Springer, 1994,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   142
\newblock LNCS 828
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   143
4985
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
   144
\bibitem{paulson-final}
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
   145
Paulson, L.~C.,
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
   146
\newblock A concrete final coalgebra theorem for {ZF} set theory,
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
   147
\newblock In Dybjer et~al. \cite{types94}, pp.~120--139
aaaf64da9e3a auto update
paulson
parents: 4585
diff changeset
   148
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   149
\bibitem{paulson-set-II}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   150
Paulson, L.~C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   151
\newblock Set theory for verification: {II}. {Induction} and recursion,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   152
\newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   153
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   154
\bibitem{paulson-coind}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   155
Paulson, L.~C.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   156
\newblock Mechanizing coinduction and corecursion in higher-order logic,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   157
\newblock {\em J. Logic and Comput. {\bf 7}}, 2 (Mar. 1997), 175--204
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   158
4058
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   159
\bibitem{paulson-markt}
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   160
Paulson, L.~C.,
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   161
\newblock Tool support for logics of programs,
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   162
\newblock In {\em Mathematical Methods in Program Development: Summer School
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   163
  Marktoberdorf 1996}, M.~Broy, Ed., NATO ASI Series F. Springer, Published
4585
9e7a32dfc1f2 Updated MOD reference
paulson
parents: 4058
diff changeset
   164
  1997, pp.~461--498
4058
18fea4aa9625 Auto update
paulson
parents: 3162
diff changeset
   165
3162
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   166
\bibitem{paulson-gr}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   167
Paulson, L.~C., Gr\c{a}bczewski, K.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   168
\newblock Mechanizing set theory: Cardinal arithmetic and the axiom of choice,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   169
\newblock {\em J. Auto. Reas. {\bf 17}}, 3 (Dec. 1996), 291--323
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   170
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   171
\bibitem{pitts94}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   172
Pitts, A.~M.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   173
\newblock A co-induction principle for recursively defined domains,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   174
\newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   175
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   176
\bibitem{rasmussen95}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   177
Rasmussen, O.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   178
\newblock The {Church-Rosser} theorem in {Isabelle}: A proof porting
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   179
  experiment,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   180
\newblock Tech. Rep. 364, Computer Laboratory, University of Cambridge, May
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   181
  1995
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   182
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   183
\bibitem{saaltink-fme}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   184
Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   185
\newblock An {EVES} data abstraction example,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   186
\newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   187
  J.~C.~P. Woodcock P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   188
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   189
\bibitem{slind-tfl}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   190
Slind, K.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   191
\newblock Function definition in higher-order logic,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   192
\newblock In {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96\/}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   193
  (1996), J.~von Wright, J.~Grundy, J.~Harrison, Eds., LNCS 1125
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   194
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   195
\bibitem{szasz93}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   196
Szasz, N.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   197
\newblock A machine checked proof that {Ackermann's} function is not primitive
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   198
  recursive,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   199
\newblock In {\em Logical Environments}, G.~Huet G.~Plotkin, Eds. Cambridge
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   200
  Univ. Press, 1993, pp.~317--338
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   201
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   202
\bibitem{voelker95}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   203
V\"olker, N.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   204
\newblock On the representation of datatypes in {Isabelle/HOL},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   205
\newblock In {\em Proceedings of the First Isabelle Users Workshop\/} (Sept.
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   206
  1995), L.~C. Paulson, Ed., Technical Report 379, Comp. Lab., Univ. Cambridge,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   207
  pp.~206--218
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   208
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   209
\bibitem{winskel93}
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   210
Winskel, G.,
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   211
\newblock {\em The Formal Semantics of Programming Languages},
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   212
\newblock MIT Press, 1993
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   213
78fa85d44e68 moved here from ..
wenzelm
parents:
diff changeset
   214
\end{thebibliography}