@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}

}