neuper@42272
|
1 |
@proceedings{DBLP:conf/mkm/2007,
|
neuper@42272
|
2 |
editor = {Manuel Kauers and
|
neuper@42272
|
3 |
Manfred Kerber and
|
neuper@42272
|
4 |
Robert Miner and
|
neuper@42272
|
5 |
Wolfgang Windsteiger},
|
neuper@42272
|
6 |
title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
|
neuper@42272
|
7 |
Calculemus 2007, 6th International Conference, MKM 2007,
|
neuper@42272
|
8 |
Hagenberg, Austria, June 27-30, 2007, Proceedings},
|
neuper@42272
|
9 |
booktitle = {Calculemus/MKM},
|
neuper@42272
|
10 |
publisher = {Springer},
|
neuper@42272
|
11 |
series = {Lecture Notes in Computer Science},
|
neuper@42272
|
12 |
volume = {4573},
|
neuper@42272
|
13 |
year = {2007},
|
neuper@42272
|
14 |
isbn = {978-3-540-73083-5},
|
neuper@42272
|
15 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
16 |
}
|
neuper@42272
|
17 |
|
neuper@42272
|
18 |
@proceedings{DBLP:conf/cade/2006,
|
neuper@42272
|
19 |
editor = {Ulrich Furbach and
|
neuper@42272
|
20 |
Natarajan Shankar},
|
neuper@42272
|
21 |
title = {Automated Reasoning, Third International Joint Conference,
|
neuper@42272
|
22 |
IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
|
neuper@42272
|
23 |
booktitle = {IJCAR},
|
neuper@42272
|
24 |
publisher = {Springer},
|
neuper@42272
|
25 |
series = {Lecture Notes in Computer Science},
|
neuper@42272
|
26 |
volume = {4130},
|
neuper@42272
|
27 |
year = {2006},
|
neuper@42272
|
28 |
isbn = {3-540-37187-7},
|
neuper@42272
|
29 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
30 |
}
|
neuper@42272
|
31 |
|
neuper@42272
|
32 |
@proceedings{DBLP:conf/iwfm/1999,
|
neuper@42272
|
33 |
editor = {Andrew Butterfield and
|
neuper@42272
|
34 |
Klemens Haegele},
|
neuper@42272
|
35 |
title = {3rd Irish Workshop on Formal Methods, Galway, Eire, July
|
neuper@42272
|
36 |
1999},
|
neuper@42272
|
37 |
booktitle = {IWFM},
|
neuper@42272
|
38 |
publisher = {BCS},
|
neuper@42272
|
39 |
series = {Workshops in Computing},
|
neuper@42272
|
40 |
year = {1999},
|
neuper@42272
|
41 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
42 |
}
|
neuper@42272
|
43 |
|
neuper@42272
|
44 |
@proceedings{DBLP:conf/aisc/2008,
|
neuper@42272
|
45 |
editor = {Serge Autexier and
|
neuper@42272
|
46 |
John Campbell and
|
neuper@42272
|
47 |
Julio Rubio and
|
neuper@42272
|
48 |
Volker Sorge and
|
neuper@42272
|
49 |
Masakazu Suzuki and
|
neuper@42272
|
50 |
Freek Wiedijk},
|
neuper@42272
|
51 |
title = {Intelligent Computer Mathematics, 9th International Conference,
|
neuper@42272
|
52 |
AISC 2008, 15th Symposium, Calculemus 2008, 7th International
|
neuper@42272
|
53 |
Conference, MKM 2008, Birmingham, UK, July 28 - August 1,
|
neuper@42272
|
54 |
2008. Proceedings},
|
neuper@42272
|
55 |
booktitle = {AISC/MKM/Calculemus},
|
neuper@42272
|
56 |
publisher = {Springer},
|
neuper@42272
|
57 |
series = {Lecture Notes in Computer Science},
|
neuper@42272
|
58 |
volume = {5144},
|
neuper@42272
|
59 |
year = {2008},
|
neuper@42272
|
60 |
isbn = {978-3-540-85109-7},
|
neuper@42272
|
61 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
62 |
}
|
neuper@42272
|
63 |
|
neuper@42272
|
64 |
@InProceedings{wn:lucas-interp-12,
|
neuper@42272
|
65 |
author = {Neuper, Walther},
|
neuper@42272
|
66 |
title = {Automated Generation of User Guidance by Combining Computation and Deduction},
|
neuper@42272
|
67 |
booktitle = {THedu'11: CTP-compontents for educational software},
|
neuper@42272
|
68 |
year = {2012},
|
neuper@42272
|
69 |
editor = {Quaresma, Pedro},
|
neuper@42272
|
70 |
publisher = {EPTCS},
|
neuper@42272
|
71 |
note = {To appear}
|
neuper@42272
|
72 |
}
|
neuper@42272
|
73 |
|
neuper@42272
|
74 |
@InProceedings{davenp-multival-10,
|
neuper@42272
|
75 |
author = {Davenport, James},
|
neuper@42272
|
76 |
title = {The Challenges of Multivalued "Functions"},
|
neuper@42272
|
77 |
booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},
|
neuper@42272
|
78 |
year = {2010}
|
neuper@42272
|
79 |
}
|
neuper@42272
|
80 |
|
neuper@42272
|
81 |
@PhdThesis{cezary-phd,
|
neuper@42272
|
82 |
author = {Kalisyk, Cezary},
|
neuper@42275
|
83 |
title = {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web},
|
neuper@42275
|
84 |
school = {Radboud University Nijmegen},
|
neuper@42275
|
85 |
year = {2009},
|
neuper@42275
|
86 |
type = {IPA Dissertation Series 2009-18},
|
neuper@42275
|
87 |
note = {Promotor Herman Geuvers}
|
neuper@42272
|
88 |
}
|
neuper@42272
|
89 |
|
neuper@42272
|
90 |
@Book{bb-loos,
|
neuper@42272
|
91 |
editor = {Buchberger, Bruno and Collins, George Edwin and Loos,
|
neuper@42272
|
92 |
R\"udiger and Albrecht, Rudolf},
|
neuper@42272
|
93 |
title = {Computer Algebra. Symbolic and Algebraic Computation},
|
neuper@42272
|
94 |
publisher = {Springer Verlag},
|
neuper@42272
|
95 |
year = {1982},
|
neuper@42272
|
96 |
edition = {2}
|
neuper@42272
|
97 |
}
|
neuper@42272
|
98 |
|
neuper@42272
|
99 |
@Book{term-nets,
|
neuper@42272
|
100 |
author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},
|
neuper@42272
|
101 |
title = {Artificial Intelligence Programming},
|
neuper@42272
|
102 |
publisher = {Lawrence Erlbaum Associates},
|
neuper@42272
|
103 |
year = {1980},
|
neuper@42272
|
104 |
note = {(Chapter 14)}
|
neuper@42272
|
105 |
}
|
neuper@42272
|
106 |
|
neuper@42272
|
107 |
@Book{db:dom-eng,
|
neuper@42272
|
108 |
author = {Bj{\o}rner, Dines},
|
neuper@42272
|
109 |
title = {Domain Engineering. Technology Management, Research and Engineering},
|
neuper@42272
|
110 |
publisher = {JAIST Press},
|
neuper@42272
|
111 |
year = {2009},
|
neuper@42272
|
112 |
month = {Feb},
|
neuper@42272
|
113 |
series = {COE Research Monograph Series},
|
neuper@42272
|
114 |
volume = {4},
|
neuper@42272
|
115 |
address = {Nomi, Japan}
|
neuper@42272
|
116 |
}
|
neuper@42272
|
117 |
|
neuper@42272
|
118 |
@techreport{harr:thesis,
|
neuper@42272
|
119 |
author={Harrison, John R.},
|
neuper@42272
|
120 |
title={Theorem proving with the real numbers},
|
neuper@42272
|
121 |
institution={University of Cambridge, Computer Laboratory},year={1996},
|
neuper@42272
|
122 |
type={Technical Report},number={408},address={},month={November},
|
neuper@42272
|
123 |
note={},status={},source={},location={loc?}
|
neuper@42272
|
124 |
}
|
neuper@42272
|
125 |
|
neuper@42272
|
126 |
@InProceedings{damas-milner-82,
|
neuper@42272
|
127 |
author = {Damas, Luis and Milner, Robin},
|
neuper@42272
|
128 |
title = {Principal type-schemes for functional programs},
|
neuper@42272
|
129 |
booktitle = {9th Symposium on Principles of programming languages (POPL'82)},
|
neuper@42272
|
130 |
pages = {207-212},
|
neuper@42272
|
131 |
year = {1982},
|
neuper@42272
|
132 |
editor = {ACM}
|
neuper@42272
|
133 |
}
|
neuper@42272
|
134 |
|
neuper@42272
|
135 |
@Article{Milner-78,
|
neuper@42272
|
136 |
author = {Milner, R.},
|
neuper@42272
|
137 |
title = {A Theory of Type Polymorphism in Programming},
|
neuper@42272
|
138 |
journal = {Journal of Computer and System Science (JCSS)},
|
neuper@42272
|
139 |
year = {1978},
|
neuper@42272
|
140 |
number = {17},
|
neuper@42272
|
141 |
pages = {348-374}
|
neuper@42272
|
142 |
}
|
neuper@42272
|
143 |
|
neuper@42272
|
144 |
@Article{Hindley-69,
|
neuper@42272
|
145 |
author = {Hindley, R.},
|
neuper@42272
|
146 |
title = {The Principal Type-Scheme of an Object in Combinatory Logic},
|
neuper@42272
|
147 |
journal = {Transactions of the American Mathematical Society},
|
neuper@42272
|
148 |
year = {1969},
|
neuper@42272
|
149 |
volume = {146},
|
neuper@42272
|
150 |
pages = {29-60}
|
neuper@42272
|
151 |
}
|
neuper@42272
|
152 |
|
neuper@42272
|
153 |
@article{seeingroots,
|
neuper@42272
|
154 |
author = {Jeffrey, D.J. and Norman, A.C.},
|
neuper@42272
|
155 |
title = {Not seeing the roots for the branches: multivalued functions in computer algebra},
|
neuper@42272
|
156 |
journal = {SIGSAM Bull.},
|
neuper@42272
|
157 |
volume = {38},
|
neuper@42272
|
158 |
number = {3},
|
neuper@42272
|
159 |
year = {2004},
|
neuper@42272
|
160 |
issn = {0163-5824},
|
neuper@42272
|
161 |
pages = {57--66},
|
neuper@42272
|
162 |
doi = {http://doi.acm.org/10.1145/1040034.1040036},
|
neuper@42272
|
163 |
publisher = {ACM},
|
neuper@42272
|
164 |
address = {New York, NY, USA},
|
neuper@42272
|
165 |
}
|
neuper@42272
|
166 |
|
neuper@42272
|
167 |
@PhdThesis{russellphd,
|
neuper@42272
|
168 |
author = {Russell O'Connor},
|
neuper@42272
|
169 |
title = {Incompleteness and Completeness.},
|
neuper@42272
|
170 |
school = {Radboud University Nijmegen},
|
neuper@42272
|
171 |
year = {2009},
|
neuper@42272
|
172 |
}
|
neuper@42272
|
173 |
|
neuper@42272
|
174 |
@inproceedings{caspartial,
|
neuper@42272
|
175 |
author = {Cezary Kaliszyk},
|
neuper@42272
|
176 |
title = {Automating Side Conditions in Formalized Partial Functions},
|
neuper@42272
|
177 |
booktitle = {AISC/MKM/Calculemus},
|
neuper@42272
|
178 |
year = {2008},
|
neuper@42272
|
179 |
pages = {300-314},
|
neuper@42272
|
180 |
ee = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},
|
neuper@42272
|
181 |
crossref = {DBLP:conf/aisc/2008},
|
neuper@42272
|
182 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
183 |
}
|
neuper@42272
|
184 |
|
neuper@42272
|
185 |
@inproceedings{farmer,
|
neuper@42272
|
186 |
author = {Farmer, William M.},
|
neuper@42272
|
187 |
title = {A Scheme for Defining Partial Higher-Order Functions by
|
neuper@42272
|
188 |
Recursion.},
|
neuper@42272
|
189 |
booktitle = {IWFM},
|
neuper@42272
|
190 |
year = {1999},
|
neuper@42272
|
191 |
crossref = {DBLP:conf/iwfm/1999},
|
neuper@42272
|
192 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
193 |
}
|
neuper@42272
|
194 |
|
neuper@42272
|
195 |
@inproceedings{krauss,
|
neuper@42272
|
196 |
author = {Krauss, Alexander},
|
neuper@42272
|
197 |
title = {Partial Recursive Functions in Higher-Order Logic},
|
neuper@42272
|
198 |
booktitle = {IJCAR},
|
neuper@42272
|
199 |
year = {2006},
|
neuper@42272
|
200 |
pages = {589-603},
|
neuper@42272
|
201 |
ee = {http://dx.doi.org/10.1007/11814771_48},
|
neuper@42272
|
202 |
crossref = {DBLP:conf/cade/2006},
|
neuper@42272
|
203 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
204 |
}
|
neuper@42272
|
205 |
|
neuper@42272
|
206 |
@inproceedings{casproto,
|
neuper@42272
|
207 |
author = {Cezary Kaliszyk and
|
neuper@42272
|
208 |
Freek Wiedijk},
|
neuper@42272
|
209 |
title = {Certified Computer Algebra on Top of an Interactive Theorem
|
neuper@42272
|
210 |
Prover},
|
neuper@42272
|
211 |
booktitle = {Calculemus},
|
neuper@42272
|
212 |
year = {2007},
|
neuper@42272
|
213 |
pages = {94-105},
|
neuper@42272
|
214 |
ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
|
neuper@42272
|
215 |
crossref = {DBLP:conf/mkm/2007},
|
neuper@42272
|
216 |
bibsource = {DBLP, http://dblp.uni-trier.de}
|
neuper@42272
|
217 |
}
|
neuper@42272
|
218 |
|
neuper@42272
|
219 |
@inproceedings{theorema00,
|
neuper@42272
|
220 |
author = "Buchberger, B. and
|
neuper@42272
|
221 |
Dupre, C. and
|
neuper@42272
|
222 |
Jebelean, T. and
|
neuper@42272
|
223 |
Kriftner, F. and
|
neuper@42272
|
224 |
Nakagawa, K. and
|
neuper@42272
|
225 |
Vasaru, D. and
|
neuper@42272
|
226 |
Windsteiger, W.",
|
neuper@42272
|
227 |
title = "{The Theorema Project: A Progress Report}",
|
neuper@42272
|
228 |
booktitle = "Symbolic Computation and Automated Reasoning
|
neuper@42272
|
229 |
(Proceedings of CALCULEMUS 2000, Symposium on the Integration of
|
neuper@42272
|
230 |
Symbolic Computation and Mechanized Reasoning)",
|
neuper@42272
|
231 |
editor = "Kerber, M. and
|
neuper@42272
|
232 |
Kohlhase, M.",
|
neuper@42272
|
233 |
publisher = "A.K.~Peters",
|
neuper@42272
|
234 |
address = "Natick, Massachusetts",
|
neuper@42272
|
235 |
isbn = "1-56881-145-4",
|
neuper@42272
|
236 |
year = 2000
|
neuper@42272
|
237 |
}
|
neuper@42272
|
238 |
|
neuper@42272
|
239 |
@inproceedings{logicalaxiom,
|
neuper@42272
|
240 |
author = {E. Poll and S. Thompson},
|
neuper@42272
|
241 |
title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},
|
neuper@42272
|
242 |
booktitle = {Calculemus and Types '98},
|
neuper@42272
|
243 |
year = {1998},
|
neuper@42272
|
244 |
place = {Eindhoven, The Netherlands},
|
neuper@42272
|
245 |
month = {July},
|
neuper@42272
|
246 |
note = {Also as technical report 6-98, Computing Laboratory, University of Kent}
|
neuper@42272
|
247 |
}
|
neuper@42272
|
248 |
|
neuper@42272
|
249 |
@InProceedings{pvs,
|
neuper@42272
|
250 |
author = {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},
|
neuper@42272
|
251 |
title = {{PVS}: Combining specification, proof checking, and model checking},
|
neuper@42272
|
252 |
booktitle = {Computer-Aided Verification},
|
neuper@42272
|
253 |
pages = {411-414},
|
neuper@42272
|
254 |
year = {1996},
|
neuper@42272
|
255 |
editor = {Alur, R. and Henzinger, T.A.},
|
neuper@42272
|
256 |
organization = {CAV'96},
|
neuper@42272
|
257 |
annote = {}
|
neuper@42272
|
258 |
}
|
neuper@42272
|
259 |
|
neuper@42272
|
260 |
@Book{Nipkow-Paulson-Wenzel:2002,
|
neuper@42272
|
261 |
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
neuper@42272
|
262 |
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
|
neuper@42272
|
263 |
publisher = {Springer},
|
neuper@42272
|
264 |
series = {LNCS},
|
neuper@42272
|
265 |
volume = 2283,
|
neuper@42272
|
266 |
year = 2002
|
neuper@42272
|
267 |
}
|
neuper@42272
|
268 |
|
neuper@42272
|
269 |
@Manual{Huet_all:94,
|
neuper@42272
|
270 |
author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},
|
neuper@42272
|
271 |
title = {The Coq Proof Assistant},
|
neuper@42272
|
272 |
institution = {INRIA-Rocquencourt},
|
neuper@42272
|
273 |
year = {1994},
|
neuper@42272
|
274 |
type = {Tutorial},
|
neuper@42272
|
275 |
number = {Version 5.10},
|
neuper@42272
|
276 |
address = {CNRS-ENS Lyon},
|
neuper@42272
|
277 |
status={},source={Theorema},location={-}
|
neuper@42272
|
278 |
}
|
neuper@42272
|
279 |
|
neuper@42272
|
280 |
@Book{einf-funct-progr,
|
neuper@42272
|
281 |
author = {Richard Bird and Philip Wadler},
|
neuper@42272
|
282 |
title = {Introduction to Functional Programming},
|
neuper@42272
|
283 |
publisher = {Prentice Hall},
|
neuper@42272
|
284 |
year = 1988,
|
neuper@42272
|
285 |
editor = {C. A. R. Hoare},
|
neuper@42272
|
286 |
series = {Prentice Hall International Series in Computer Science},
|
neuper@42272
|
287 |
address = {New York, London, Toronto, Sydney, Tokyo},
|
neuper@42272
|
288 |
annote = {88bok371}
|
neuper@42272
|
289 |
}
|
neuper@42272
|
290 |
@Book{Winkler:96,
|
neuper@42272
|
291 |
author = {F. Winkler},
|
neuper@42272
|
292 |
title = {{Polynomial Algorithms in Computer Algebra}},
|
neuper@42272
|
293 |
publisher = {Springer-Verlag Wien New York},
|
neuper@42272
|
294 |
year = {1996}
|
neuper@42272
|
295 |
}
|
neuper@42272
|
296 |
|