diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/dmeindl/references.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-isac/dmeindl/references.bib Tue Sep 17 09:50:52 2013 +0200 @@ -0,0 +1,296 @@ +@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} +} +