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