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