doc-src/Logics/logics.bbl
changeset 878 7c82ab7602b4
parent 707 04d661f1d2f8
child 1054 f3fabffd927a
equal deleted inserted replaced
877:e528724951b0 878:7c82ab7602b4
   163 \bibitem{paulson87}
   163 \bibitem{paulson87}
   164 Lawrence~C. Paulson.
   164 Lawrence~C. Paulson.
   165 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   165 \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   166 \newblock Cambridge University Press, 1987.
   166 \newblock Cambridge University Press, 1987.
   167 
   167 
   168 \bibitem{paulson-COLOG}
       
   169 Lawrence~C. Paulson.
       
   170 \newblock A formulation of the simple theory of types (for {Isabelle}).
       
   171 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
       
   172   International Conference on Computer Logic}, Tallinn, 1990. Estonian Academy
       
   173   of Sciences, Springer.
       
   174 \newblock LNCS 417.
       
   175 
       
   176 \bibitem{paulson-coind}
   168 \bibitem{paulson-coind}
   177 Lawrence~C. Paulson.
   169 Lawrence~C. Paulson.
   178 \newblock Co-induction and co-recursion in higher-order logic.
   170 \newblock Co-induction and co-recursion in higher-order logic.
   179 \newblock Technical Report 304, Computer Laboratory, University of Cambridge,
   171 \newblock Technical Report 304, Computer Laboratory, University of Cambridge,
   180   July 1993.
   172   July 1993.
   199 
   191 
   200 \bibitem{paulson-CADE}
   192 \bibitem{paulson-CADE}
   201 Lawrence~C. Paulson.
   193 Lawrence~C. Paulson.
   202 \newblock A fixedpoint approach to implementing (co)inductive definitions.
   194 \newblock A fixedpoint approach to implementing (co)inductive definitions.
   203 \newblock In Alan Bundy, editor, {\em 12th International Conference on
   195 \newblock In Alan Bundy, editor, {\em 12th International Conference on
   204   Automated Deduction}, pages 148--161. Springer, 1994.
   196   Automated Deduction}, volume 814, pages 148--161. Springer, 1994.
   205 \newblock LNAI 814.
   197 
       
   198 \bibitem{paulson-COLOG}
       
   199 Lawrence~C. Paulson.
       
   200 \newblock A formulation of the simple theory of types (for {Isabelle}).
       
   201 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
       
   202   International Conference on Computer Logic}, pages 246--274, Tallinn,
       
   203   Published 1990. Estonian Academy of Sciences, Springer.
       
   204 \newblock LNCS 417.
   206 
   205 
   207 \bibitem{pelletier86}
   206 \bibitem{pelletier86}
   208 F.~J. Pelletier.
   207 F.~J. Pelletier.
   209 \newblock Seventy-five problems for testing automatic theorem provers.
   208 \newblock Seventy-five problems for testing automatic theorem provers.
   210 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   209 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   226 \newblock Dover, 1972.
   225 \newblock Dover, 1972.
   227 
   226 
   228 \bibitem{takeuti87}
   227 \bibitem{takeuti87}
   229 G.~Takeuti.
   228 G.~Takeuti.
   230 \newblock {\em Proof Theory}.
   229 \newblock {\em Proof Theory}.
   231 \newblock North Holland, 2nd edition, 1987.
   230 \newblock North-Holland, 2nd edition, 1987.
   232 
   231 
   233 \bibitem{thompson91}
   232 \bibitem{thompson91}
   234 Simon Thompson.
   233 Simon Thompson.
   235 \newblock {\em Type Theory and Functional Programming}.
   234 \newblock {\em Type Theory and Functional Programming}.
   236 \newblock Addison-Wesley, 1991.
   235 \newblock Addison-Wesley, 1991.