neuper@42272: @proceedings{DBLP:conf/mkm/2007, neuper@42272: editor = {Manuel Kauers and neuper@42272: Manfred Kerber and neuper@42272: Robert Miner and neuper@42272: Wolfgang Windsteiger}, neuper@42272: title = {Towards Mechanized Mathematical Assistants, 14th Symposium, neuper@42272: Calculemus 2007, 6th International Conference, MKM 2007, neuper@42272: Hagenberg, Austria, June 27-30, 2007, Proceedings}, neuper@42272: booktitle = {Calculemus/MKM}, neuper@42272: publisher = {Springer}, neuper@42272: series = {Lecture Notes in Computer Science}, neuper@42272: volume = {4573}, neuper@42272: year = {2007}, neuper@42272: isbn = {978-3-540-73083-5}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @proceedings{DBLP:conf/cade/2006, neuper@42272: editor = {Ulrich Furbach and neuper@42272: Natarajan Shankar}, neuper@42272: title = {Automated Reasoning, Third International Joint Conference, neuper@42272: IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings}, neuper@42272: booktitle = {IJCAR}, neuper@42272: publisher = {Springer}, neuper@42272: series = {Lecture Notes in Computer Science}, neuper@42272: volume = {4130}, neuper@42272: year = {2006}, neuper@42272: isbn = {3-540-37187-7}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @proceedings{DBLP:conf/iwfm/1999, neuper@42272: editor = {Andrew Butterfield and neuper@42272: Klemens Haegele}, neuper@42272: title = {3rd Irish Workshop on Formal Methods, Galway, Eire, July neuper@42272: 1999}, neuper@42272: booktitle = {IWFM}, neuper@42272: publisher = {BCS}, neuper@42272: series = {Workshops in Computing}, neuper@42272: year = {1999}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @proceedings{DBLP:conf/aisc/2008, neuper@42272: editor = {Serge Autexier and neuper@42272: John Campbell and neuper@42272: Julio Rubio and neuper@42272: Volker Sorge and neuper@42272: Masakazu Suzuki and neuper@42272: Freek Wiedijk}, neuper@42272: title = {Intelligent Computer Mathematics, 9th International Conference, neuper@42272: AISC 2008, 15th Symposium, Calculemus 2008, 7th International neuper@42272: Conference, MKM 2008, Birmingham, UK, July 28 - August 1, neuper@42272: 2008. Proceedings}, neuper@42272: booktitle = {AISC/MKM/Calculemus}, neuper@42272: publisher = {Springer}, neuper@42272: series = {Lecture Notes in Computer Science}, neuper@42272: volume = {5144}, neuper@42272: year = {2008}, neuper@42272: isbn = {978-3-540-85109-7}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @InProceedings{wn:lucas-interp-12, neuper@42272: author = {Neuper, Walther}, neuper@42272: title = {Automated Generation of User Guidance by Combining Computation and Deduction}, neuper@42272: booktitle = {THedu'11: CTP-compontents for educational software}, neuper@42272: year = {2012}, neuper@42272: editor = {Quaresma, Pedro}, neuper@42272: publisher = {EPTCS}, neuper@42272: note = {To appear} neuper@42272: } neuper@42272: neuper@42272: @InProceedings{davenp-multival-10, neuper@42272: author = {Davenport, James}, neuper@42272: title = {The Challenges of Multivalued "Functions"}, neuper@42272: booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)}, neuper@42272: year = {2010} neuper@42272: } neuper@42272: neuper@42272: @PhdThesis{cezary-phd, neuper@42272: author = {Kalisyk, Cezary}, neuper@42275: title = {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web}, neuper@42275: school = {Radboud University Nijmegen}, neuper@42275: year = {2009}, neuper@42275: type = {IPA Dissertation Series 2009-18}, neuper@42275: note = {Promotor Herman Geuvers} neuper@42272: } neuper@42272: neuper@42272: @Book{bb-loos, neuper@42272: editor = {Buchberger, Bruno and Collins, George Edwin and Loos, neuper@42272: R\"udiger and Albrecht, Rudolf}, neuper@42272: title = {Computer Algebra. Symbolic and Algebraic Computation}, neuper@42272: publisher = {Springer Verlag}, neuper@42272: year = {1982}, neuper@42272: edition = {2} neuper@42272: } neuper@42272: neuper@42272: @Book{term-nets, neuper@42272: author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.}, neuper@42272: title = {Artificial Intelligence Programming}, neuper@42272: publisher = {Lawrence Erlbaum Associates}, neuper@42272: year = {1980}, neuper@42272: note = {(Chapter 14)} neuper@42272: } neuper@42272: neuper@42272: @Book{db:dom-eng, neuper@42272: author = {Bj{\o}rner, Dines}, neuper@42272: title = {Domain Engineering. Technology Management, Research and Engineering}, neuper@42272: publisher = {JAIST Press}, neuper@42272: year = {2009}, neuper@42272: month = {Feb}, neuper@42272: series = {COE Research Monograph Series}, neuper@42272: volume = {4}, neuper@42272: address = {Nomi, Japan} neuper@42272: } neuper@42272: neuper@42272: @techreport{harr:thesis, neuper@42272: author={Harrison, John R.}, neuper@42272: title={Theorem proving with the real numbers}, neuper@42272: institution={University of Cambridge, Computer Laboratory},year={1996}, neuper@42272: type={Technical Report},number={408},address={},month={November}, neuper@42272: note={},status={},source={},location={loc?} neuper@42272: } neuper@42272: neuper@42272: @InProceedings{damas-milner-82, neuper@42272: author = {Damas, Luis and Milner, Robin}, neuper@42272: title = {Principal type-schemes for functional programs}, neuper@42272: booktitle = {9th Symposium on Principles of programming languages (POPL'82)}, neuper@42272: pages = {207-212}, neuper@42272: year = {1982}, neuper@42272: editor = {ACM} neuper@42272: } neuper@42272: neuper@42272: @Article{Milner-78, neuper@42272: author = {Milner, R.}, neuper@42272: title = {A Theory of Type Polymorphism in Programming}, neuper@42272: journal = {Journal of Computer and System Science (JCSS)}, neuper@42272: year = {1978}, neuper@42272: number = {17}, neuper@42272: pages = {348-374} neuper@42272: } neuper@42272: neuper@42272: @Article{Hindley-69, neuper@42272: author = {Hindley, R.}, neuper@42272: title = {The Principal Type-Scheme of an Object in Combinatory Logic}, neuper@42272: journal = {Transactions of the American Mathematical Society}, neuper@42272: year = {1969}, neuper@42272: volume = {146}, neuper@42272: pages = {29-60} neuper@42272: } neuper@42272: neuper@42272: @article{seeingroots, neuper@42272: author = {Jeffrey, D.J. and Norman, A.C.}, neuper@42272: title = {Not seeing the roots for the branches: multivalued functions in computer algebra}, neuper@42272: journal = {SIGSAM Bull.}, neuper@42272: volume = {38}, neuper@42272: number = {3}, neuper@42272: year = {2004}, neuper@42272: issn = {0163-5824}, neuper@42272: pages = {57--66}, neuper@42272: doi = {http://doi.acm.org/10.1145/1040034.1040036}, neuper@42272: publisher = {ACM}, neuper@42272: address = {New York, NY, USA}, neuper@42272: } neuper@42272: neuper@42272: @PhdThesis{russellphd, neuper@42272: author = {Russell O'Connor}, neuper@42272: title = {Incompleteness and Completeness.}, neuper@42272: school = {Radboud University Nijmegen}, neuper@42272: year = {2009}, neuper@42272: } neuper@42272: neuper@42272: @inproceedings{caspartial, neuper@42272: author = {Cezary Kaliszyk}, neuper@42272: title = {Automating Side Conditions in Formalized Partial Functions}, neuper@42272: booktitle = {AISC/MKM/Calculemus}, neuper@42272: year = {2008}, neuper@42272: pages = {300-314}, neuper@42272: ee = {http://dx.doi.org/10.1007/978-3-540-85110-3_26}, neuper@42272: crossref = {DBLP:conf/aisc/2008}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @inproceedings{farmer, neuper@42272: author = {Farmer, William M.}, neuper@42272: title = {A Scheme for Defining Partial Higher-Order Functions by neuper@42272: Recursion.}, neuper@42272: booktitle = {IWFM}, neuper@42272: year = {1999}, neuper@42272: crossref = {DBLP:conf/iwfm/1999}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @inproceedings{krauss, neuper@42272: author = {Krauss, Alexander}, neuper@42272: title = {Partial Recursive Functions in Higher-Order Logic}, neuper@42272: booktitle = {IJCAR}, neuper@42272: year = {2006}, neuper@42272: pages = {589-603}, neuper@42272: ee = {http://dx.doi.org/10.1007/11814771_48}, neuper@42272: crossref = {DBLP:conf/cade/2006}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @inproceedings{casproto, neuper@42272: author = {Cezary Kaliszyk and neuper@42272: Freek Wiedijk}, neuper@42272: title = {Certified Computer Algebra on Top of an Interactive Theorem neuper@42272: Prover}, neuper@42272: booktitle = {Calculemus}, neuper@42272: year = {2007}, neuper@42272: pages = {94-105}, neuper@42272: ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8}, neuper@42272: crossref = {DBLP:conf/mkm/2007}, neuper@42272: bibsource = {DBLP, http://dblp.uni-trier.de} neuper@42272: } neuper@42272: neuper@42272: @inproceedings{theorema00, neuper@42272: author = "Buchberger, B. and neuper@42272: Dupre, C. and neuper@42272: Jebelean, T. and neuper@42272: Kriftner, F. and neuper@42272: Nakagawa, K. and neuper@42272: Vasaru, D. and neuper@42272: Windsteiger, W.", neuper@42272: title = "{The Theorema Project: A Progress Report}", neuper@42272: booktitle = "Symbolic Computation and Automated Reasoning neuper@42272: (Proceedings of CALCULEMUS 2000, Symposium on the Integration of neuper@42272: Symbolic Computation and Mechanized Reasoning)", neuper@42272: editor = "Kerber, M. and neuper@42272: Kohlhase, M.", neuper@42272: publisher = "A.K.~Peters", neuper@42272: address = "Natick, Massachusetts", neuper@42272: isbn = "1-56881-145-4", neuper@42272: year = 2000 neuper@42272: } neuper@42272: neuper@42272: @inproceedings{logicalaxiom, neuper@42272: author = {E. Poll and S. Thompson}, neuper@42272: title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}}, neuper@42272: booktitle = {Calculemus and Types '98}, neuper@42272: year = {1998}, neuper@42272: place = {Eindhoven, The Netherlands}, neuper@42272: month = {July}, neuper@42272: note = {Also as technical report 6-98, Computing Laboratory, University of Kent} neuper@42272: } neuper@42272: neuper@42272: @InProceedings{pvs, neuper@42272: author = {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.}, neuper@42272: title = {{PVS}: Combining specification, proof checking, and model checking}, neuper@42272: booktitle = {Computer-Aided Verification}, neuper@42272: pages = {411-414}, neuper@42272: year = {1996}, neuper@42272: editor = {Alur, R. and Henzinger, T.A.}, neuper@42272: organization = {CAV'96}, neuper@42272: annote = {} neuper@42272: } neuper@42272: neuper@42272: @Book{Nipkow-Paulson-Wenzel:2002, neuper@42272: author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, neuper@42272: title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic}, neuper@42272: publisher = {Springer}, neuper@42272: series = {LNCS}, neuper@42272: volume = 2283, neuper@42272: year = 2002 neuper@42272: } neuper@42272: neuper@42272: @Manual{Huet_all:94, neuper@42272: author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.}, neuper@42272: title = {The Coq Proof Assistant}, neuper@42272: institution = {INRIA-Rocquencourt}, neuper@42272: year = {1994}, neuper@42272: type = {Tutorial}, neuper@42272: number = {Version 5.10}, neuper@42272: address = {CNRS-ENS Lyon}, neuper@42272: status={},source={Theorema},location={-} neuper@42272: } neuper@42272: neuper@42272: @Book{einf-funct-progr, neuper@42272: author = {Richard Bird and Philip Wadler}, neuper@42272: title = {Introduction to Functional Programming}, neuper@42272: publisher = {Prentice Hall}, neuper@42272: year = 1988, neuper@42272: editor = {C. A. R. Hoare}, neuper@42272: series = {Prentice Hall International Series in Computer Science}, neuper@42272: address = {New York, London, Toronto, Sydney, Tokyo}, neuper@42272: annote = {88bok371} neuper@42272: } neuper@42272: @Book{Winkler:96, neuper@42272: author = {F. Winkler}, neuper@42272: title = {{Polynomial Algorithms in Computer Algebra}}, neuper@42272: publisher = {Springer-Verlag Wien New York}, neuper@42272: year = {1996} neuper@42272: } neuper@42272: