1 @proceedings{DBLP:conf/mkm/2007,
2 editor = {Manuel Kauers and
6 title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
7 Calculemus 2007, 6th International Conference, MKM 2007,
8 Hagenberg, Austria, June 27-30, 2007, Proceedings},
9 booktitle = {Calculemus/MKM},
10 publisher = {Springer},
11 series = {Lecture Notes in Computer Science},
14 isbn = {978-3-540-73083-5},
15 bibsource = {DBLP, http://dblp.uni-trier.de}
18 @proceedings{DBLP:conf/cade/2006,
19 editor = {Ulrich Furbach and
21 title = {Automated Reasoning, Third International Joint Conference,
22 IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
24 publisher = {Springer},
25 series = {Lecture Notes in Computer Science},
28 isbn = {3-540-37187-7},
29 bibsource = {DBLP, http://dblp.uni-trier.de}
32 @proceedings{DBLP:conf/iwfm/1999,
33 editor = {Andrew Butterfield and
35 title = {3rd Irish Workshop on Formal Methods, Galway, Eire, July
39 series = {Workshops in Computing},
41 bibsource = {DBLP, http://dblp.uni-trier.de}
44 @proceedings{DBLP:conf/aisc/2008,
45 editor = {Serge Autexier and
51 title = {Intelligent Computer Mathematics, 9th International Conference,
52 AISC 2008, 15th Symposium, Calculemus 2008, 7th International
53 Conference, MKM 2008, Birmingham, UK, July 28 - August 1,
55 booktitle = {AISC/MKM/Calculemus},
56 publisher = {Springer},
57 series = {Lecture Notes in Computer Science},
60 isbn = {978-3-540-85109-7},
61 bibsource = {DBLP, http://dblp.uni-trier.de}
64 @InProceedings{wn:lucas-interp-12,
65 author = {Neuper, Walther},
66 title = {Automated Generation of User Guidance by Combining Computation and Deduction},
67 booktitle = {THedu'11: CTP-compontents for educational software},
69 editor = {Quaresma, Pedro},
74 @InProceedings{davenp-multival-10,
75 author = {Davenport, James},
76 title = {The Challenges of Multivalued "Functions"},
77 booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},
81 @PhdThesis{cezary-phd,
82 author = {Kalisyk, Cezary},
95 editor = {Buchberger, Bruno and Collins, George Edwin and Loos,
96 R\"udiger and Albrecht, Rudolf},
97 title = {Computer Algebra. Symbolic and Algebraic Computation},
98 publisher = {Springer Verlag},
104 author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},
105 title = {Artificial Intelligence Programming},
106 publisher = {Lawrence Erlbaum Associates},
108 note = {(Chapter 14)}
112 author = {Bj{\o}rner, Dines},
113 title = {Domain Engineering. Technology Management, Research and Engineering},
114 publisher = {JAIST Press},
117 series = {COE Research Monograph Series},
119 address = {Nomi, Japan}
122 @techreport{harr:thesis,
123 author={Harrison, John R.},
124 title={Theorem proving with the real numbers},
125 institution={University of Cambridge, Computer Laboratory},year={1996},
126 type={Technical Report},number={408},address={},month={November},
127 note={},status={},source={},location={loc?}
130 @InProceedings{damas-milner-82,
131 author = {Damas, Luis and Milner, Robin},
132 title = {Principal type-schemes for functional programs},
133 booktitle = {9th Symposium on Principles of programming languages (POPL'82)},
140 author = {Milner, R.},
141 title = {A Theory of Type Polymorphism in Programming},
142 journal = {Journal of Computer and System Science (JCSS)},
149 author = {Hindley, R.},
150 title = {The Principal Type-Scheme of an Object in Combinatory Logic},
151 journal = {Transactions of the American Mathematical Society},
157 @article{seeingroots,
158 author = {Jeffrey, D.J. and Norman, A.C.},
159 title = {Not seeing the roots for the branches: multivalued functions in computer algebra},
160 journal = {SIGSAM Bull.},
166 doi = {http://doi.acm.org/10.1145/1040034.1040036},
168 address = {New York, NY, USA},
171 @PhdThesis{russellphd,
172 author = {Russell O'Connor},
173 title = {Incompleteness and Completeness.},
174 school = {Radboud University Nijmegen},
178 @inproceedings{caspartial,
179 author = {Cezary Kaliszyk},
180 title = {Automating Side Conditions in Formalized Partial Functions},
181 booktitle = {AISC/MKM/Calculemus},
184 ee = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},
185 crossref = {DBLP:conf/aisc/2008},
186 bibsource = {DBLP, http://dblp.uni-trier.de}
189 @inproceedings{farmer,
190 author = {Farmer, William M.},
191 title = {A Scheme for Defining Partial Higher-Order Functions by
195 crossref = {DBLP:conf/iwfm/1999},
196 bibsource = {DBLP, http://dblp.uni-trier.de}
199 @inproceedings{krauss,
200 author = {Krauss, Alexander},
201 title = {Partial Recursive Functions in Higher-Order Logic},
205 ee = {http://dx.doi.org/10.1007/11814771_48},
206 crossref = {DBLP:conf/cade/2006},
207 bibsource = {DBLP, http://dblp.uni-trier.de}
210 @inproceedings{casproto,
211 author = {Cezary Kaliszyk and
213 title = {Certified Computer Algebra on Top of an Interactive Theorem
215 booktitle = {Calculemus},
218 ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
219 crossref = {DBLP:conf/mkm/2007},
220 bibsource = {DBLP, http://dblp.uni-trier.de}
223 @inproceedings{theorema00,
224 author = "Buchberger, B. and
231 title = "{The Theorema Project: A Progress Report}",
232 booktitle = "Symbolic Computation and Automated Reasoning
233 (Proceedings of CALCULEMUS 2000, Symposium on the Integration of
234 Symbolic Computation and Mechanized Reasoning)",
235 editor = "Kerber, M. and
237 publisher = "A.K.~Peters",
238 address = "Natick, Massachusetts",
239 isbn = "1-56881-145-4",
243 @inproceedings{logicalaxiom,
244 author = {E. Poll and S. Thompson},
245 title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},
246 booktitle = {Calculemus and Types '98},
248 place = {Eindhoven, The Netherlands},
250 note = {Also as technical report 6-98, Computing Laboratory, University of Kent}
254 author = {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},
255 title = {{PVS}: Combining specification, proof checking, and model checking},
256 booktitle = {Computer-Aided Verification},
259 editor = {Alur, R. and Henzinger, T.A.},
260 organization = {CAV'96},
264 @Book{Nipkow-Paulson-Wenzel:2002,
265 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
266 title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
267 publisher = {Springer},
274 author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},
275 title = {The Coq Proof Assistant},
276 institution = {INRIA-Rocquencourt},
279 number = {Version 5.10},
280 address = {CNRS-ENS Lyon},
281 status={},source={Theorema},location={-}
284 @Book{einf-funct-progr,
285 author = {Richard Bird and Philip Wadler},
286 title = {Introduction to Functional Programming},
287 publisher = {Prentice Hall},
289 editor = {C. A. R. Hoare},
290 series = {Prentice Hall International Series in Computer Science},
291 address = {New York, London, Toronto, Sydney, Tokyo},
295 author = {F. Winkler},
296 title = {{Polynomial Algorithms in Computer Algebra}},
297 publisher = {Springer-Verlag Wien New York},