diff -r 3ec847562782 -r 1fead823c7c6 doc-src/springer.bbl
--- a/doc-src/springer.bbl	Tue Aug 28 13:12:03 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{andrews86}
-Andrews, P.~B.,
-\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
-  Through Proof},
-\newblock Academic Press, 1986
-
-\bibitem{basin91}
-Basin, D., Kaufmann, M.,
-\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
-\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
-  Univ. Press, 1991, pp.~89--119
-
-\bibitem{boyer86}
-Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
-\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
-\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
-
-\bibitem{bm88book}
-Boyer, R.~S., Moore, J.~S.,
-\newblock {\em A Computational Logic Handbook},
-\newblock Academic Press, 1988
-
-\bibitem{camilleri92}
-Camilleri, J., Melham, T.~F.,
-\newblock Reasoning with inductively defined relations in the {HOL} theorem
-  prover,
-\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
-
-\bibitem{charniak80}
-Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
-\newblock {\em Artificial Intelligence Programming},
-\newblock Lawrence Erlbaum Associates, 1980
-
-\bibitem{church40}
-Church, A.,
-\newblock A formulation of the simple theory of types,
-\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
-
-\bibitem{coen92}
-Coen, M.~D.,
-\newblock {\em Interactive Program Derivation},
-\newblock PhD thesis, University of Cambridge, 1992,
-\newblock Computer Laboratory Technical Report 272
-
-\bibitem{constable86}
-{Constable et al.}, R.~L.,
-\newblock {\em Implementing Mathematics with the Nuprl Proof Development
-  System},
-\newblock Prentice-Hall, 1986
-
-\bibitem{davey&priestley}
-Davey, B.~A., Priestley, H.~A.,
-\newblock {\em Introduction to Lattices and Order},
-\newblock Cambridge Univ. Press, 1990
-
-\bibitem{dawson90}
-Dawson, W.~M.,
-\newblock {\em A Generic Logic Environment},
-\newblock PhD thesis, Imperial College, London, 1990
-
-\bibitem{debruijn72}
-de~Bruijn, N.~G.,
-\newblock Lambda calculus notation with nameless dummies, a tool for automatic
-  formula manipulation, with application to the {Church-Rosser Theorem},
-\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
-
-\bibitem{devlin79}
-Devlin, K.~J.,
-\newblock {\em Fundamentals of Contemporary Set Theory},
-\newblock Springer, 1979
-
-\bibitem{coq}
-{Dowek et al.}, G.,
-\newblock The {Coq} proof assistant user's guide,
-\newblock Technical Report 134, INRIA-Rocquencourt, 1991
-
-\bibitem{dummett}
-Dummett, M.,
-\newblock {\em Elements of Intuitionism},
-\newblock Oxford University Press, 1977
-
-\bibitem{dyckhoff}
-Dyckhoff, R.,
-\newblock Contraction-free sequent calculi for intuitionistic logic,
-\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
-
-\bibitem{felty91a}
-Felty, A.,
-\newblock A logic program for transforming sequent proofs to natural deduction
-  proofs,
-\newblock In {\em Extensions of Logic Programming\/} (1991),
-  P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
-\newblock LNAI 475
-
-\bibitem{felty93}
-Felty, A.,
-\newblock Implementing tactics and tacticals in a higher-order logic
-  programming language,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
-
-\bibitem{frost93}
-Frost, J.,
-\newblock A case study of co-induction in {Isabelle HOL},
-\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
-
-\bibitem{OBJ}
-Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
-\newblock Principles of {OBJ2},
-\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
-
-\bibitem{gallier86}
-Gallier, J.~H.,
-\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
-  Proving},
-\newblock Harper \& Row, 1986
-
-\bibitem{mgordon-hol}
-Gordon, M. J.~C., Melham, T.~F.,
-\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
-  Order Logic},
-\newblock Cambridge Univ. Press, 1993
-
-\bibitem{halmos60}
-Halmos, P.~R.,
-\newblock {\em Naive Set Theory},
-\newblock Van Nostrand, 1960
-
-\bibitem{harper-jacm}
-Harper, R., Honsell, F., Plotkin, G.,
-\newblock A framework for defining logics,
-\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
-
-\bibitem{haskell-tutorial}
-Hudak, P., Fasel, J.~H.,
-\newblock A gentle introduction to {Haskell},
-\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
-
-\bibitem{haskell-report}
-Hudak, P., Jones, S.~P., Wadler, P.,
-\newblock Report on the programming language {Haskell}: A non-strict, purely
-  functional language,
-\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
-\newblock Version 1.2
-
-\bibitem{huet75}
-Huet, G.~P.,
-\newblock A unification algorithm for typed $\lambda$-calculus,
-\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
-
-\bibitem{huet78}
-Huet, G.~P., Lang, B.,
-\newblock Proving and applying program transformations expressed with
-  second-order patterns,
-\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
-
-\bibitem{mural}
-Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
-\newblock {\em Mural: A Formal Development Support System},
-\newblock Springer, 1991
-
-\bibitem{alf}
-Magnusson, L., {Nordstr\"om}, B.,
-\newblock The {ALF} proof editor and its proof engine,
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '93}\/} (published 1994), Springer, pp.~213--237,
-\newblock LNCS 806
-
-\bibitem{mw81}
-Manna, Z., Waldinger, R.,
-\newblock Deductive synthesis of the unification algorithm,
-\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
-
-\bibitem{martin-nipkow}
-Martin, U., Nipkow, T.,
-\newblock Ordered rewriting and confluence,
-\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
-  Springer, pp.~366--380,
-\newblock LNCS 449
-
-\bibitem{martinlof84}
-Martin-L\"of, P.,
-\newblock {\em Intuitionistic type theory},
-\newblock Bibliopolis, 1984
-
-\bibitem{melham89}
-Melham, T.~F.,
-\newblock Automating recursive type definitions in higher order logic,
-\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
-  Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
-  pp.~341--386
-
-\bibitem{miller-mixed}
-Miller, D.,
-\newblock Unification under a mixed prefix,
-\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
-
-\bibitem{milner-coind}
-Milner, R., Tofte, M.,
-\newblock Co-induction in relational semantics,
-\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
-
-\bibitem{nipkow-prehofer}
-Nipkow, T., Prehofer, C.,
-\newblock Type checking type classes,
-\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
-\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
-
-\bibitem{noel}
-{No\"el}, P.,
-\newblock Experimenting with {Isabelle} in {ZF} set theory,
-\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
-
-\bibitem{nordstrom90}
-{Nordstr\"om}, B., Petersson, K., Smith, J.,
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
-\newblock Oxford University Press, 1990
-
-\bibitem{paulin92}
-Paulin-Mohring, C.,
-\newblock Inductive definitions in the system {Coq}: Rules and properties,
-\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
-  1992
-
-\bibitem{paulson85}
-Paulson, L.~C.,
-\newblock Verifying the unification algorithm in {LCF},
-\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
-
-\bibitem{paulson87}
-Paulson, L.~C.,
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
-\newblock Cambridge Univ. Press, 1987
-
-\bibitem{paulson89}
-Paulson, L.~C.,
-\newblock The foundation of a generic theorem prover,
-\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
-
-\bibitem{paulson-COLOG}
-Paulson, L.~C.,
-\newblock A formulation of the simple theory of types (for {Isabelle}),
-\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
-  (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
-  Sciences, Springer,
-\newblock LNCS 417
-
-\bibitem{paulson700}
-Paulson, L.~C.,
-\newblock {Isabelle}: The next 700 theorem provers,
-\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
-  Press, 1990, pp.~361--386
-
-\bibitem{paulson91}
-Paulson, L.~C.,
-\newblock {\em {ML} for the Working Programmer},
-\newblock Cambridge Univ. Press, 1991
-
-\bibitem{paulson-coind}
-Paulson, L.~C.,
-\newblock Co-induction and co-recursion in higher-order logic,
-\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
-
-\bibitem{paulson-fixedpt}
-Paulson, L.~C.,
-\newblock A fixedpoint approach to implementing (co)inductive definitions,
-\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
-
-\bibitem{paulson-set-I}
-Paulson, L.~C.,
-\newblock Set theory for verification: {I}. {From} foundations to functions,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
-
-\bibitem{paulson-set-II}
-Paulson, L.~C.,
-\newblock Set theory for verification: {II}. {Induction} and recursion,
-\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
-
-\bibitem{paulson-final}
-Paulson, L.~C.,
-\newblock A concrete final coalgebra theorem for {ZF} set theory,
-\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
-
-\bibitem{pelletier86}
-Pelletier, F.~J.,
-\newblock Seventy-five problems for testing automatic theorem provers,
-\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
-\newblock Errata, JAR 4 (1988), 235--236
-
-\bibitem{plaisted90}
-Plaisted, D.~A.,
-\newblock A sequent-style model elimination strategy and a positive refinement,
-\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
-
-\bibitem{quaife92}
-Quaife, A.,
-\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
-\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
-
-\bibitem{sawamura92}
-Sawamura, H., Minami, T., Ohashi, K.,
-\newblock Proof methods based on sheet of thought in {EUODHILOS},
-\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
-  Study of Social Information Science, Fujitsu Laboratories, 1992
-
-\bibitem{suppes72}
-Suppes, P.,
-\newblock {\em Axiomatic Set Theory},
-\newblock Dover, 1972
-
-\bibitem{takeuti87}
-Takeuti, G.,
-\newblock {\em Proof Theory}, 2nd~ed.,
-\newblock North Holland, 1987
-
-\bibitem{thompson91}
-Thompson, S.,
-\newblock {\em Type Theory and Functional Programming},
-\newblock Addison-Wesley, 1991
-
-\bibitem{principia}
-Whitehead, A.~N., Russell, B.,
-\newblock {\em Principia Mathematica},
-\newblock Cambridge Univ. Press, 1962,
-\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
-
-\bibitem{wos-bledsoe}
-Wos, L.,
-\newblock Automated reasoning and {Bledsoe's} dream for the field,
-\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
-  R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
-
-\end{thebibliography}