|
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 = {TODO}, |
|
84 school = {}, |
|
85 year = {}, |
|
86 OPTkey = {}, |
|
87 OPTtype = {}, |
|
88 OPTaddress = {}, |
|
89 OPTmonth = {}, |
|
90 OPTnote = {}, |
|
91 OPTannote = {} |
|
92 } |
|
93 |
|
94 @Book{bb-loos, |
|
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}, |
|
99 year = {1982}, |
|
100 edition = {2} |
|
101 } |
|
102 |
|
103 @Book{term-nets, |
|
104 author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.}, |
|
105 title = {Artificial Intelligence Programming}, |
|
106 publisher = {Lawrence Erlbaum Associates}, |
|
107 year = {1980}, |
|
108 note = {(Chapter 14)} |
|
109 } |
|
110 |
|
111 @Book{db:dom-eng, |
|
112 author = {Bj{\o}rner, Dines}, |
|
113 title = {Domain Engineering. Technology Management, Research and Engineering}, |
|
114 publisher = {JAIST Press}, |
|
115 year = {2009}, |
|
116 month = {Feb}, |
|
117 series = {COE Research Monograph Series}, |
|
118 volume = {4}, |
|
119 address = {Nomi, Japan} |
|
120 } |
|
121 |
|
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?} |
|
128 } |
|
129 |
|
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)}, |
|
134 pages = {207-212}, |
|
135 year = {1982}, |
|
136 editor = {ACM} |
|
137 } |
|
138 |
|
139 @Article{Milner-78, |
|
140 author = {Milner, R.}, |
|
141 title = {A Theory of Type Polymorphism in Programming}, |
|
142 journal = {Journal of Computer and System Science (JCSS)}, |
|
143 year = {1978}, |
|
144 number = {17}, |
|
145 pages = {348-374} |
|
146 } |
|
147 |
|
148 @Article{Hindley-69, |
|
149 author = {Hindley, R.}, |
|
150 title = {The Principal Type-Scheme of an Object in Combinatory Logic}, |
|
151 journal = {Transactions of the American Mathematical Society}, |
|
152 year = {1969}, |
|
153 volume = {146}, |
|
154 pages = {29-60} |
|
155 } |
|
156 |
|
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.}, |
|
161 volume = {38}, |
|
162 number = {3}, |
|
163 year = {2004}, |
|
164 issn = {0163-5824}, |
|
165 pages = {57--66}, |
|
166 doi = {http://doi.acm.org/10.1145/1040034.1040036}, |
|
167 publisher = {ACM}, |
|
168 address = {New York, NY, USA}, |
|
169 } |
|
170 |
|
171 @PhdThesis{russellphd, |
|
172 author = {Russell O'Connor}, |
|
173 title = {Incompleteness and Completeness.}, |
|
174 school = {Radboud University Nijmegen}, |
|
175 year = {2009}, |
|
176 } |
|
177 |
|
178 @inproceedings{caspartial, |
|
179 author = {Cezary Kaliszyk}, |
|
180 title = {Automating Side Conditions in Formalized Partial Functions}, |
|
181 booktitle = {AISC/MKM/Calculemus}, |
|
182 year = {2008}, |
|
183 pages = {300-314}, |
|
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} |
|
187 } |
|
188 |
|
189 @inproceedings{farmer, |
|
190 author = {Farmer, William M.}, |
|
191 title = {A Scheme for Defining Partial Higher-Order Functions by |
|
192 Recursion.}, |
|
193 booktitle = {IWFM}, |
|
194 year = {1999}, |
|
195 crossref = {DBLP:conf/iwfm/1999}, |
|
196 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
197 } |
|
198 |
|
199 @inproceedings{krauss, |
|
200 author = {Krauss, Alexander}, |
|
201 title = {Partial Recursive Functions in Higher-Order Logic}, |
|
202 booktitle = {IJCAR}, |
|
203 year = {2006}, |
|
204 pages = {589-603}, |
|
205 ee = {http://dx.doi.org/10.1007/11814771_48}, |
|
206 crossref = {DBLP:conf/cade/2006}, |
|
207 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
208 } |
|
209 |
|
210 @inproceedings{casproto, |
|
211 author = {Cezary Kaliszyk and |
|
212 Freek Wiedijk}, |
|
213 title = {Certified Computer Algebra on Top of an Interactive Theorem |
|
214 Prover}, |
|
215 booktitle = {Calculemus}, |
|
216 year = {2007}, |
|
217 pages = {94-105}, |
|
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} |
|
221 } |
|
222 |
|
223 @inproceedings{theorema00, |
|
224 author = "Buchberger, B. and |
|
225 Dupre, C. and |
|
226 Jebelean, T. and |
|
227 Kriftner, F. and |
|
228 Nakagawa, K. and |
|
229 Vasaru, D. and |
|
230 Windsteiger, W.", |
|
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 |
|
236 Kohlhase, M.", |
|
237 publisher = "A.K.~Peters", |
|
238 address = "Natick, Massachusetts", |
|
239 isbn = "1-56881-145-4", |
|
240 year = 2000 |
|
241 } |
|
242 |
|
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}, |
|
247 year = {1998}, |
|
248 place = {Eindhoven, The Netherlands}, |
|
249 month = {July}, |
|
250 note = {Also as technical report 6-98, Computing Laboratory, University of Kent} |
|
251 } |
|
252 |
|
253 @InProceedings{pvs, |
|
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}, |
|
257 pages = {411-414}, |
|
258 year = {1996}, |
|
259 editor = {Alur, R. and Henzinger, T.A.}, |
|
260 organization = {CAV'96}, |
|
261 annote = {} |
|
262 } |
|
263 |
|
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}, |
|
268 series = {LNCS}, |
|
269 volume = 2283, |
|
270 year = 2002 |
|
271 } |
|
272 |
|
273 @Manual{Huet_all:94, |
|
274 author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.}, |
|
275 title = {The Coq Proof Assistant}, |
|
276 institution = {INRIA-Rocquencourt}, |
|
277 year = {1994}, |
|
278 type = {Tutorial}, |
|
279 number = {Version 5.10}, |
|
280 address = {CNRS-ENS Lyon}, |
|
281 status={},source={Theorema},location={-} |
|
282 } |
|
283 |
|
284 @Book{einf-funct-progr, |
|
285 author = {Richard Bird and Philip Wadler}, |
|
286 title = {Introduction to Functional Programming}, |
|
287 publisher = {Prentice Hall}, |
|
288 year = 1988, |
|
289 editor = {C. A. R. Hoare}, |
|
290 series = {Prentice Hall International Series in Computer Science}, |
|
291 address = {New York, London, Toronto, Sydney, Tokyo}, |
|
292 annote = {88bok371} |
|
293 } |
|
294 @Book{Winkler:96, |
|
295 author = {F. Winkler}, |
|
296 title = {{Polynomial Algorithms in Computer Algebra}}, |
|
297 publisher = {Springer-Verlag Wien New York}, |
|
298 year = {1996} |
|
299 } |
|
300 |