doc-src/ind-defs.bbl
changeset 1444 23ceb1dc9755
parent 1184 94ada3b54caa
child 1535 681a5d04393e
equal deleted inserted replaced
1443:ff8a804e0201 1444:23ceb1dc9755
    53 
    53 
    54 \bibitem{huet88}
    54 \bibitem{huet88}
    55 Huet, G.,
    55 Huet, G.,
    56 \newblock Induction principles formalized in the {Calculus of Constructions},
    56 \newblock Induction principles formalized in the {Calculus of Constructions},
    57 \newblock In {\em Programming of Future Generation Computers\/} (1988),
    57 \newblock In {\em Programming of Future Generation Computers\/} (1988),
    58   Elsevier, pp.~205--216
    58   K.~Fuchi, M.~Nivat, Eds., Elsevier, pp.~205--216
    59 
    59 
    60 \bibitem{melham89}
    60 \bibitem{melham89}
    61 Melham, T.~F.,
    61 Melham, T.~F.,
    62 \newblock Automating recursive type definitions in higher order logic,
    62 \newblock Automating recursive type definitions in higher order logic,
    63 \newblock In {\em Current Trends in Hardware Verification and Automated Theorem
    63 \newblock In {\em Current Trends in Hardware Verification and Automated Theorem
    96 \newblock Cambridge Univ. Press, 1991
    96 \newblock Cambridge Univ. Press, 1991
    97 
    97 
    98 \bibitem{paulson-coind}
    98 \bibitem{paulson-coind}
    99 Paulson, L.~C.,
    99 Paulson, L.~C.,
   100 \newblock Co-induction and co-recursion in higher-order logic,
   100 \newblock Co-induction and co-recursion in higher-order logic,
   101 \newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
   101 \newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993,
       
   102 \newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson
       
   103   and M. Zeleny
   102 
   104 
   103 \bibitem{isabelle-intro}
   105 \bibitem{isabelle-intro}
   104 Paulson, L.~C.,
   106 Paulson, L.~C.,
   105 \newblock Introduction to {Isabelle},
   107 \newblock Introduction to {Isabelle},
   106 \newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
   108 \newblock Tech. Rep. 280, Comp. Lab., Univ. Cambridge, 1993
   111 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
   113 \newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
   112 
   114 
   113 \bibitem{paulson-set-II}
   115 \bibitem{paulson-set-II}
   114 Paulson, L.~C.,
   116 Paulson, L.~C.,
   115 \newblock Set theory for verification: {II}. {Induction} and recursion,
   117 \newblock Set theory for verification: {II}. {Induction} and recursion,
   116 \newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993,
   118 \newblock {\em J. Auto. Reas. {\bf 15}}, 2 (1995), 167--215
   117 \newblock To appear in J. Auto. Reas.
       
   118 
   119 
   119 \bibitem{paulson-final}
   120 \bibitem{paulson-final}
   120 Paulson, L.~C.,
   121 Paulson, L.~C.,
   121 \newblock A concrete final coalgebra theorem for {ZF} set theory,
   122 \newblock A concrete final coalgebra theorem for {ZF} set theory,
   122 \newblock Tech. Rep. 334, Comp. Lab., Univ. Cambridge, 1994
   123 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
       
   124   '94}\/} (published 1995), P.~Dybjer, B.~Nordstr{\"om},, J.~Smith, Eds., LNCS
       
   125   996, Springer, pp.~120--139
   123 
   126 
   124 \bibitem{pitts94}
   127 \bibitem{pitts94}
   125 Pitts, A.~M.,
   128 Pitts, A.~M.,
   126 \newblock A co-induction principle for recursively defined domains,
   129 \newblock A co-induction principle for recursively defined domains,
   127 \newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
   130 \newblock {\em Theoretical Comput. Sci. {\bf 124}\/} (1994), 195--219
   128 
   131 
   129 \bibitem{saaltink-fme}
   132 \bibitem{saaltink-fme}
   130 Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
   133 Saaltink, M., Kromodimoeljo, S., Pase, B., Craigen, D., Meisels, I.,
   131 \newblock An {EVES} data abstraction example,
   134 \newblock An {EVES} data abstraction example,
   132 \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
   135 \newblock In {\em FME '93: Industrial-Strength Formal Methods\/} (1993),
   133   J.~C.~P. Woodcock, P.~G. Larsen, Eds., Springer, pp.~578--596,
   136   J.~C.~P. Woodcock, P.~G. Larsen, Eds., LNCS 670, Springer, pp.~578--596
   134 \newblock LNCS 670
       
   135 
   137 
   136 \bibitem{szasz93}
   138 \bibitem{szasz93}
   137 Szasz, N.,
   139 Szasz, N.,
   138 \newblock A machine checked proof that {Ackermann's} function is not primitive
   140 \newblock A machine checked proof that {Ackermann's} function is not primitive
   139   recursive,
   141   recursive,