@proceedings{DBLP:conf/mkm/2007,

   editor    = {Manuel Kauers and

                Manfred Kerber and

                Robert Miner and

                Wolfgang Windsteiger},

   title     = {Towards Mechanized Mathematical Assistants, 14th Symposium,

                Calculemus 2007, 6th International Conference, MKM 2007,

                Hagenberg, Austria, June 27-30, 2007, Proceedings},

   booktitle = {Calculemus/MKM},

   publisher = {Springer},

   series    = {Lecture Notes in Computer Science},

   volume    = {4573},

   year      = {2007},

   isbn      = {978-3-540-73083-5},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @proceedings{DBLP:conf/cade/2006,

   editor    = {Ulrich Furbach and

                Natarajan Shankar},

   title     = {Automated Reasoning, Third International Joint Conference,

                IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},

   booktitle = {IJCAR},

   publisher = {Springer},

   series    = {Lecture Notes in Computer Science},

   volume    = {4130},

   year      = {2006},

   isbn      = {3-540-37187-7},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @proceedings{DBLP:conf/iwfm/1999,

   editor    = {Andrew Butterfield and

                Klemens Haegele},

   title     = {3rd Irish Workshop on Formal Methods, Galway, Eire, July

                1999},

   booktitle = {IWFM},

   publisher = {BCS},

   series    = {Workshops in Computing},

   year      = {1999},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @proceedings{DBLP:conf/aisc/2008,

   editor    = {Serge Autexier and

                John Campbell and

                Julio Rubio and

                Volker Sorge and

                Masakazu Suzuki and

                Freek Wiedijk},

   title     = {Intelligent Computer Mathematics, 9th International Conference,

                AISC 2008, 15th Symposium, Calculemus 2008, 7th International

                Conference, MKM 2008, Birmingham, UK, July 28 - August 1,

                2008. Proceedings},

   booktitle = {AISC/MKM/Calculemus},

   publisher = {Springer},

   series    = {Lecture Notes in Computer Science},

   volume    = {5144},

   year      = {2008},

   isbn      = {978-3-540-85109-7},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @InProceedings{wn:lucas-interp-12,

   author = 	 {Neuper, Walther},

   title = 	 {Automated Generation of User Guidance by Combining Computation and Deduction},

   booktitle = {THedu'11: CTP-compontents for educational software},

   year = 	 {2012},

   editor = 	 {Quaresma, Pedro},

   publisher = {EPTCS},

   note = {To appear}

 }

 @InProceedings{davenp-multival-10,

   author = 	 {Davenport, James},

   title = 	 {The Challenges of Multivalued "Functions"},

   booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},

   year = 	 {2010}

 }

 @PhdThesis{cezary-phd,

   author = 	 {Kalisyk, Cezary},

   title = 	 {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web},

   school = 	 {Radboud University Nijmegen},

   year = 	 {2009},

   type = 	 {IPA Dissertation Series 2009-18},

   note = 	 {Promotor Herman Geuvers}

 }

 @Book{bb-loos,

   editor = 	 {Buchberger, Bruno and Collins, George Edwin and Loos, 

                   R\"udiger and Albrecht, Rudolf},

   title = 	 {Computer Algebra. Symbolic and Algebraic Computation},

   publisher = 	 {Springer Verlag},

   year = 	 {1982},

   edition = 	 {2}

 }

 @Book{term-nets,

   author = 	 {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},

   title = 	 {Artificial Intelligence Programming},

   publisher = 	 {Lawrence Erlbaum Associates},

   year = 	 {1980},

   note = 	 {(Chapter 14)}

 }

 @Book{db:dom-eng,

   author = 	 {Bj{\o}rner, Dines},

   title = 	 {Domain Engineering. Technology Management, Research and Engineering},

   publisher = 	 {JAIST Press},

   year = 	 {2009},

   month = 	 {Feb},

   series = 	 {COE Research Monograph Series},

   volume = 	 {4},

   address = 	 {Nomi, Japan}

 }

 @techreport{harr:thesis,

         author={Harrison, John R.},

         title={Theorem proving with the real numbers},

         institution={University of Cambridge, Computer Laboratory},year={1996}, 

         type={Technical Report},number={408},address={},month={November},

         note={},status={},source={},location={loc?} 

         }  

 @InProceedings{damas-milner-82,

   author = 	 {Damas, Luis and Milner, Robin},

   title = 	 {Principal type-schemes for functional programs},

   booktitle = {9th Symposium on Principles of programming languages (POPL'82)},

   pages = 	 {207-212},

   year = 	 {1982},

   editor = 	 {ACM}

 }

 @Article{Milner-78,

   author = 	 {Milner, R.},

   title = 	 {A Theory of Type Polymorphism in Programming},

   journal = 	 {Journal of Computer and System Science (JCSS)},

   year = 	 {1978},

   number = 	 {17},

   pages = 	 {348-374}

 }

 @Article{Hindley-69,

   author = 	 {Hindley, R.},

   title = 	 {The Principal Type-Scheme of an Object in Combinatory Logic},

   journal = 	 {Transactions of the American Mathematical Society},

   year = 	 {1969},

   volume = 	 {146},

   pages = 	 {29-60}

 }

 @article{seeingroots,

  author = {Jeffrey, D.J. and Norman, A.C.},

  title = {Not seeing the roots for the branches: multivalued functions in computer algebra},

  journal = {SIGSAM Bull.},

  volume = {38},

  number = {3},

  year = {2004},

  issn = {0163-5824},

  pages = {57--66},

  doi = {http://doi.acm.org/10.1145/1040034.1040036},

  publisher = {ACM},

  address = {New York, NY, USA},

  }

 @PhdThesis{russellphd,

   author =       {Russell O'Connor},

   title =        {Incompleteness and Completeness.},

   school =       {Radboud University Nijmegen},

   year =         {2009},

 }

 @inproceedings{caspartial,

   author    = {Cezary Kaliszyk},

   title     = {Automating Side Conditions in Formalized Partial Functions},

   booktitle = {AISC/MKM/Calculemus},

   year      = {2008},

   pages     = {300-314},

   ee        = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},

   crossref  = {DBLP:conf/aisc/2008},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{farmer,

   author    = {Farmer, William M.},

   title     = {A Scheme for Defining Partial Higher-Order Functions by

                Recursion.},

   booktitle = {IWFM},

   year      = {1999},

   crossref  = {DBLP:conf/iwfm/1999},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{krauss,

   author    = {Krauss, Alexander},

   title     = {Partial Recursive Functions in Higher-Order Logic},

   booktitle = {IJCAR},

   year      = {2006},

   pages     = {589-603},

   ee        = {http://dx.doi.org/10.1007/11814771_48},

   crossref  = {DBLP:conf/cade/2006},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{casproto,

   author    = {Cezary Kaliszyk and

                Freek Wiedijk},

   title     = {Certified Computer Algebra on Top of an Interactive Theorem

                Prover},

   booktitle = {Calculemus},

   year      = {2007},

   pages     = {94-105},

   ee        = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},

   crossref  = {DBLP:conf/mkm/2007},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @inproceedings{theorema00,

   author = "Buchberger, B. and

     Dupre, C. and

     Jebelean, T. and

     Kriftner, F. and

     Nakagawa, K. and

     Vasaru, D. and

     Windsteiger, W.",

   title = "{The Theorema Project: A Progress Report}",

   booktitle = "Symbolic Computation and Automated Reasoning

     (Proceedings of CALCULEMUS 2000, Symposium on the Integration of

     Symbolic Computation and Mechanized Reasoning)",

   editor = "Kerber, M. and

     Kohlhase, M.",

   publisher = "A.K.~Peters",

   address = "Natick, Massachusetts",

   isbn = "1-56881-145-4",

   year = 2000

 }

 @inproceedings{logicalaxiom,

 	author = {E. Poll and S. Thompson},

 	title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},

   booktitle = {Calculemus and Types '98},

 	year = {1998},

   place = {Eindhoven, The Netherlands},

 	month = {July},

 	note = {Also as technical report 6-98, Computing Laboratory, University of Kent}

 }

 @InProceedings{pvs,

   author = 	 {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},

   title = 	 {{PVS}: Combining specification, proof checking, and model checking},

   booktitle = 	 {Computer-Aided Verification},

   pages = 	 {411-414},

   year = 	 {1996},

   editor = 	 {Alur, R. and Henzinger, T.A.},

   organization = {CAV'96},

   annote = 	 {}

 }

 @Book{Nipkow-Paulson-Wenzel:2002,

   author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},

   title		= {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},

   publisher	= {Springer},

   series	= {LNCS},

   volume	= 2283,

   year		= 2002

 }

 @Manual{Huet_all:94,

   author = 	 {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},

   title = 	 {The Coq Proof Assistant},

   institution =  {INRIA-Rocquencourt},

   year = 	 {1994},

   type = 	 {Tutorial},

   number = 	 {Version 5.10},

   address = 	 {CNRS-ENS Lyon},

   status={},source={Theorema},location={-}

 }

 @Book{einf-funct-progr,

   author = 	 {Richard Bird and Philip Wadler},

   title = 	 {Introduction to Functional Programming},

   publisher = 	 {Prentice Hall},

   year = 	 1988,

   editor =	 {C. A. R. Hoare},

   series =	 {Prentice Hall International Series in Computer Science},

   address =	 {New York, London, Toronto, Sydney, Tokyo},

   annote =	 {88bok371}

 }

 @Book{Winkler:96,

   author =       {F. Winkler},

   title =        {{Polynomial Algorithms in Computer Algebra}},

   publisher =    {Springer-Verlag Wien New York},

   year =         {1996}

 }