diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/dmeindl/references.bib --- a/src/Doc/isac/dmeindl/references.bib Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,296 +0,0 @@ -@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} -} -