1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/dmeindl/references.bib Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,296 @@
1.4 +@proceedings{DBLP:conf/mkm/2007,
1.5 + editor = {Manuel Kauers and
1.6 + Manfred Kerber and
1.7 + Robert Miner and
1.8 + Wolfgang Windsteiger},
1.9 + title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
1.10 + Calculemus 2007, 6th International Conference, MKM 2007,
1.11 + Hagenberg, Austria, June 27-30, 2007, Proceedings},
1.12 + booktitle = {Calculemus/MKM},
1.13 + publisher = {Springer},
1.14 + series = {Lecture Notes in Computer Science},
1.15 + volume = {4573},
1.16 + year = {2007},
1.17 + isbn = {978-3-540-73083-5},
1.18 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.19 +}
1.20 +
1.21 +@proceedings{DBLP:conf/cade/2006,
1.22 + editor = {Ulrich Furbach and
1.23 + Natarajan Shankar},
1.24 + title = {Automated Reasoning, Third International Joint Conference,
1.25 + IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
1.26 + booktitle = {IJCAR},
1.27 + publisher = {Springer},
1.28 + series = {Lecture Notes in Computer Science},
1.29 + volume = {4130},
1.30 + year = {2006},
1.31 + isbn = {3-540-37187-7},
1.32 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.33 +}
1.34 +
1.35 +@proceedings{DBLP:conf/iwfm/1999,
1.36 + editor = {Andrew Butterfield and
1.37 + Klemens Haegele},
1.38 + title = {3rd Irish Workshop on Formal Methods, Galway, Eire, July
1.39 + 1999},
1.40 + booktitle = {IWFM},
1.41 + publisher = {BCS},
1.42 + series = {Workshops in Computing},
1.43 + year = {1999},
1.44 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.45 +}
1.46 +
1.47 +@proceedings{DBLP:conf/aisc/2008,
1.48 + editor = {Serge Autexier and
1.49 + John Campbell and
1.50 + Julio Rubio and
1.51 + Volker Sorge and
1.52 + Masakazu Suzuki and
1.53 + Freek Wiedijk},
1.54 + title = {Intelligent Computer Mathematics, 9th International Conference,
1.55 + AISC 2008, 15th Symposium, Calculemus 2008, 7th International
1.56 + Conference, MKM 2008, Birmingham, UK, July 28 - August 1,
1.57 + 2008. Proceedings},
1.58 + booktitle = {AISC/MKM/Calculemus},
1.59 + publisher = {Springer},
1.60 + series = {Lecture Notes in Computer Science},
1.61 + volume = {5144},
1.62 + year = {2008},
1.63 + isbn = {978-3-540-85109-7},
1.64 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.65 +}
1.66 +
1.67 +@InProceedings{wn:lucas-interp-12,
1.68 + author = {Neuper, Walther},
1.69 + title = {Automated Generation of User Guidance by Combining Computation and Deduction},
1.70 + booktitle = {THedu'11: CTP-compontents for educational software},
1.71 + year = {2012},
1.72 + editor = {Quaresma, Pedro},
1.73 + publisher = {EPTCS},
1.74 + note = {To appear}
1.75 +}
1.76 +
1.77 +@InProceedings{davenp-multival-10,
1.78 + author = {Davenport, James},
1.79 + title = {The Challenges of Multivalued "Functions"},
1.80 + booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},
1.81 + year = {2010}
1.82 +}
1.83 +
1.84 +@PhdThesis{cezary-phd,
1.85 + author = {Kalisyk, Cezary},
1.86 + title = {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web},
1.87 + school = {Radboud University Nijmegen},
1.88 + year = {2009},
1.89 + type = {IPA Dissertation Series 2009-18},
1.90 + note = {Promotor Herman Geuvers}
1.91 +}
1.92 +
1.93 +@Book{bb-loos,
1.94 + editor = {Buchberger, Bruno and Collins, George Edwin and Loos,
1.95 + R\"udiger and Albrecht, Rudolf},
1.96 + title = {Computer Algebra. Symbolic and Algebraic Computation},
1.97 + publisher = {Springer Verlag},
1.98 + year = {1982},
1.99 + edition = {2}
1.100 +}
1.101 +
1.102 +@Book{term-nets,
1.103 + author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},
1.104 + title = {Artificial Intelligence Programming},
1.105 + publisher = {Lawrence Erlbaum Associates},
1.106 + year = {1980},
1.107 + note = {(Chapter 14)}
1.108 +}
1.109 +
1.110 +@Book{db:dom-eng,
1.111 + author = {Bj{\o}rner, Dines},
1.112 + title = {Domain Engineering. Technology Management, Research and Engineering},
1.113 + publisher = {JAIST Press},
1.114 + year = {2009},
1.115 + month = {Feb},
1.116 + series = {COE Research Monograph Series},
1.117 + volume = {4},
1.118 + address = {Nomi, Japan}
1.119 +}
1.120 +
1.121 +@techreport{harr:thesis,
1.122 + author={Harrison, John R.},
1.123 + title={Theorem proving with the real numbers},
1.124 + institution={University of Cambridge, Computer Laboratory},year={1996},
1.125 + type={Technical Report},number={408},address={},month={November},
1.126 + note={},status={},source={},location={loc?}
1.127 + }
1.128 +
1.129 +@InProceedings{damas-milner-82,
1.130 + author = {Damas, Luis and Milner, Robin},
1.131 + title = {Principal type-schemes for functional programs},
1.132 + booktitle = {9th Symposium on Principles of programming languages (POPL'82)},
1.133 + pages = {207-212},
1.134 + year = {1982},
1.135 + editor = {ACM}
1.136 +}
1.137 +
1.138 +@Article{Milner-78,
1.139 + author = {Milner, R.},
1.140 + title = {A Theory of Type Polymorphism in Programming},
1.141 + journal = {Journal of Computer and System Science (JCSS)},
1.142 + year = {1978},
1.143 + number = {17},
1.144 + pages = {348-374}
1.145 +}
1.146 +
1.147 +@Article{Hindley-69,
1.148 + author = {Hindley, R.},
1.149 + title = {The Principal Type-Scheme of an Object in Combinatory Logic},
1.150 + journal = {Transactions of the American Mathematical Society},
1.151 + year = {1969},
1.152 + volume = {146},
1.153 + pages = {29-60}
1.154 +}
1.155 +
1.156 +@article{seeingroots,
1.157 + author = {Jeffrey, D.J. and Norman, A.C.},
1.158 + title = {Not seeing the roots for the branches: multivalued functions in computer algebra},
1.159 + journal = {SIGSAM Bull.},
1.160 + volume = {38},
1.161 + number = {3},
1.162 + year = {2004},
1.163 + issn = {0163-5824},
1.164 + pages = {57--66},
1.165 + doi = {http://doi.acm.org/10.1145/1040034.1040036},
1.166 + publisher = {ACM},
1.167 + address = {New York, NY, USA},
1.168 + }
1.169 +
1.170 +@PhdThesis{russellphd,
1.171 + author = {Russell O'Connor},
1.172 + title = {Incompleteness and Completeness.},
1.173 + school = {Radboud University Nijmegen},
1.174 + year = {2009},
1.175 +}
1.176 +
1.177 +@inproceedings{caspartial,
1.178 + author = {Cezary Kaliszyk},
1.179 + title = {Automating Side Conditions in Formalized Partial Functions},
1.180 + booktitle = {AISC/MKM/Calculemus},
1.181 + year = {2008},
1.182 + pages = {300-314},
1.183 + ee = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},
1.184 + crossref = {DBLP:conf/aisc/2008},
1.185 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.186 +}
1.187 +
1.188 +@inproceedings{farmer,
1.189 + author = {Farmer, William M.},
1.190 + title = {A Scheme for Defining Partial Higher-Order Functions by
1.191 + Recursion.},
1.192 + booktitle = {IWFM},
1.193 + year = {1999},
1.194 + crossref = {DBLP:conf/iwfm/1999},
1.195 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.196 +}
1.197 +
1.198 +@inproceedings{krauss,
1.199 + author = {Krauss, Alexander},
1.200 + title = {Partial Recursive Functions in Higher-Order Logic},
1.201 + booktitle = {IJCAR},
1.202 + year = {2006},
1.203 + pages = {589-603},
1.204 + ee = {http://dx.doi.org/10.1007/11814771_48},
1.205 + crossref = {DBLP:conf/cade/2006},
1.206 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.207 +}
1.208 +
1.209 +@inproceedings{casproto,
1.210 + author = {Cezary Kaliszyk and
1.211 + Freek Wiedijk},
1.212 + title = {Certified Computer Algebra on Top of an Interactive Theorem
1.213 + Prover},
1.214 + booktitle = {Calculemus},
1.215 + year = {2007},
1.216 + pages = {94-105},
1.217 + ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
1.218 + crossref = {DBLP:conf/mkm/2007},
1.219 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.220 +}
1.221 +
1.222 +@inproceedings{theorema00,
1.223 + author = "Buchberger, B. and
1.224 + Dupre, C. and
1.225 + Jebelean, T. and
1.226 + Kriftner, F. and
1.227 + Nakagawa, K. and
1.228 + Vasaru, D. and
1.229 + Windsteiger, W.",
1.230 + title = "{The Theorema Project: A Progress Report}",
1.231 + booktitle = "Symbolic Computation and Automated Reasoning
1.232 + (Proceedings of CALCULEMUS 2000, Symposium on the Integration of
1.233 + Symbolic Computation and Mechanized Reasoning)",
1.234 + editor = "Kerber, M. and
1.235 + Kohlhase, M.",
1.236 + publisher = "A.K.~Peters",
1.237 + address = "Natick, Massachusetts",
1.238 + isbn = "1-56881-145-4",
1.239 + year = 2000
1.240 +}
1.241 +
1.242 +@inproceedings{logicalaxiom,
1.243 + author = {E. Poll and S. Thompson},
1.244 + title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},
1.245 + booktitle = {Calculemus and Types '98},
1.246 + year = {1998},
1.247 + place = {Eindhoven, The Netherlands},
1.248 + month = {July},
1.249 + note = {Also as technical report 6-98, Computing Laboratory, University of Kent}
1.250 +}
1.251 +
1.252 +@InProceedings{pvs,
1.253 + author = {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},
1.254 + title = {{PVS}: Combining specification, proof checking, and model checking},
1.255 + booktitle = {Computer-Aided Verification},
1.256 + pages = {411-414},
1.257 + year = {1996},
1.258 + editor = {Alur, R. and Henzinger, T.A.},
1.259 + organization = {CAV'96},
1.260 + annote = {}
1.261 +}
1.262 +
1.263 +@Book{Nipkow-Paulson-Wenzel:2002,
1.264 + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
1.265 + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
1.266 + publisher = {Springer},
1.267 + series = {LNCS},
1.268 + volume = 2283,
1.269 + year = 2002
1.270 +}
1.271 +
1.272 +@Manual{Huet_all:94,
1.273 + author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},
1.274 + title = {The Coq Proof Assistant},
1.275 + institution = {INRIA-Rocquencourt},
1.276 + year = {1994},
1.277 + type = {Tutorial},
1.278 + number = {Version 5.10},
1.279 + address = {CNRS-ENS Lyon},
1.280 + status={},source={Theorema},location={-}
1.281 +}
1.282 +
1.283 +@Book{einf-funct-progr,
1.284 + author = {Richard Bird and Philip Wadler},
1.285 + title = {Introduction to Functional Programming},
1.286 + publisher = {Prentice Hall},
1.287 + year = 1988,
1.288 + editor = {C. A. R. Hoare},
1.289 + series = {Prentice Hall International Series in Computer Science},
1.290 + address = {New York, London, Toronto, Sydney, Tokyo},
1.291 + annote = {88bok371}
1.292 +}
1.293 +@Book{Winkler:96,
1.294 + author = {F. Winkler},
1.295 + title = {{Polynomial Algorithms in Computer Algebra}},
1.296 + publisher = {Springer-Verlag Wien New York},
1.297 + year = {1996}
1.298 +}
1.299 +