doc-src/ind-defs.bbl
changeset 104 d8205bb279a7
child 293 63a0077dd9f2
equal deleted inserted replaced
103:30bd42401ab2 104:d8205bb279a7
       
     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 65--116. Addison-Wesley, 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   739--782. North-Holland, 1977.
       
    14 
       
    15 \bibitem{aczel88}
       
    16 Peter Aczel.
       
    17 \newblock {\em Non-Well-Founded 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   341--386. Springer, 1989.
       
    49 
       
    50 \bibitem{milner89}
       
    51 Robin Milner.
       
    52 \newblock {\em Communication and Concurrency}.
       
    53 \newblock Prentice-Hall, 1989.
       
    54 
       
    55 \bibitem{paulin92}
       
    56 Christine Paulin-Mohring.
       
    57 \newblock Inductive definitions in the system {Coq}: Rules and properties.
       
    58 \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
       
    59   December 1992.
       
    60 
       
    61 \bibitem{paulson-set-I}
       
    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{paulson-coind}
       
    74 Lawrence~C. Paulson.
       
    75 \newblock Co-induction and co-recursion in higher-order logic.
       
    76 \newblock Technical Report 304, University of Cambridge Computer Laboratory,
       
    77   July 1993.
       
    78 
       
    79 \bibitem{isabelle-intro}
       
    80 Lawrence~C. Paulson.
       
    81 \newblock Introduction to {Isabelle}.
       
    82 \newblock Technical Report 280, University of Cambridge Computer Laboratory,
       
    83   1993.
       
    84 
       
    85 \bibitem{paulson-set-II}
       
    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 co-induction 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 317--338. Cambridge University Press, 1993.
       
   104 
       
   105 \end{thebibliography}