|
1 |
|
2 @Proceedings{EPTCS79, |
|
3 title = {{\rm Proceedings First Workshop on} |
|
4 CTP Components for Educational Software (THedu'11)}, |
|
5 year = {2012}, |
|
6 booktitle = {Electronic Proceedings in Theoretical Computer Science}, |
|
7 editor = "Quaresma, Pedro and Back, Ralph-Johan", |
|
8 volume = "79", |
|
9 publisher = "Open Publishing Association" |
|
10 } |
|
11 @techreport{RISC5885, |
|
12 author = {David M. Cerna}, |
|
13 title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}}, |
|
14 year = {2019}, |
|
15 month = {Feburary}, |
|
16 length = {17}, |
|
17 type = {RISC Report Series}, |
|
18 institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz}, |
|
19 address = {Schloss Hagenberg, 4232 Hagenberg, Austria} |
|
20 } |
|
21 @Article{EMS-STT-19, |
|
22 author = {Koichu, Boris and Pinto, Alon}, |
|
23 title = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?}, |
|
24 journal = {EMS Newsletter}, |
|
25 year = {2019}, |
|
26 pages = {34-35}, |
|
27 month = {June}, |
|
28 doi = {10.4171/NEWS} |
|
29 } |
|
30 |
|
31 @Inproceedings{EPTCS290.6, |
|
32 author = {Neuper, Walther}, |
|
33 year = {2019}, |
|
34 title = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education}, |
|
35 editor = {Quaresma, Pedro and Neuper, Walther}, |
|
36 booktitle = {{\rm Proceedings 7th International Workshop on} |
|
37 Theorem proving components for Educational software, |
|
38 {\rm Oxford, United Kingdom, 18 july 2018}}, |
|
39 series = {Electronic Proceedings in Theoretical Computer Science}, |
|
40 volume = {290}, |
|
41 publisher = {Open Publishing Association}, |
|
42 pages = {76-95}, |
|
43 doi = {10.4204/EPTCS.290.6} |
|
44 } |
|
45 @InProceedings{wneuper:gcd-coimbra, |
|
46 author = {Neuper, Walther}, |
|
47 title = {{GCD} --- A Case Study on {L}ucas-Interpretation}, |
|
48 booktitle = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM}, |
|
49 year = {2014}, |
|
50 address = {Coimbra, Portugal}, |
|
51 month = {July 7-11}, |
|
52 note = {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}} |
|
53 } |
|
54 @Article{flip-class-meta, |
|
55 author = {Shi, Y. and Ma, Y. and MacLeod, J. and others}, |
|
56 title = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature}, |
|
57 journal = {Journal of Computers in Education}, |
|
58 year = {2019}, |
|
59 pages = {1-25}, |
|
60 month = {May}, |
|
61 doi = {https://doi.org/10.1007/s40692-019-00142-8} |
|
62 } |
|
63 @inproceedings{krauss, |
|
64 author = {Krauss, Alexander}, |
|
65 title = {Partial Recursive Functions in Higher-Order Logic}, |
|
66 pages = {589-603}, |
|
67 doi = {10.1007/11814771\_48}, |
|
68 editor = {Ulrich Furbach and Natarajan Shankar}, |
|
69 booktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006}, |
|
70 publisher = {Springer}, |
|
71 series = {Lecture Notes in Computer Science}, |
|
72 volume = {4130}, |
|
73 year = {2006}, |
|
74 bibsource = {DBLP, http://dblp.uni-trier.de} |
|
75 } |
|
76 @Manual{funpack-tutorial, |
|
77 title = {Defining Recursive Functions in {Isabelle/HOL}}, |
|
78 author = {Alexander Krauss}, |
|
79 address = {Munich}, |
|
80 year = {}, |
|
81 note = {{P}art of the Isabelle distribution}, |
|
82 url = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} |
|
83 } |
|
84 @Misc{nipkow-prog-prove-ny, |
|
85 author = {Nipkow, Tobias}, |
|
86 title = {Programming and Proving in {Isabelle/HOL}}, |
|
87 howpublished = {contained in the Isabelle distribution}, |
|
88 year = {}, |
|
89 url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}} |
|
90 } |
|
91 @Misc{code-gen-tutorial, |
|
92 author = {Florian Haftmann}, |
|
93 title = {Code generation from {Isabelle/HOL} theories}, |
|
94 howpublished = {Contained in the Isabelle distribution}, |
|
95 year = {}, |
|
96 url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}} |
|
97 } |
|
98 @Misc{implem-tutorial, |
|
99 author = {Makarius Wenzel}, |
|
100 title = {The {Isabelle/Isar} Implementation}, |
|
101 howpublished = {Contained in the Isabelle distribution}, |
|
102 year = {}, |
|
103 url = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}} |
|
104 } |
|
105 @Misc{sledgehammer-tutorial, |
|
106 author = {Jasmin C.Blanchette}, |
|
107 title = {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}}, |
|
108 howpublished = {contained in the Isabelle distribution}, |
|
109 year = {}, |
|
110 url = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}} |
|
111 } |
|
112 @incollection {haftm-nipkow-code-gen-HRS-10, |
|
113 author = {Haftmann, Florian and Nipkow, Tobias}, |
|
114 affiliation = {Institut für Informatik, Technische Universität München}, |
|
115 title = {Code Generation via Higher-Order Rewrite Systems}, |
|
116 booktitle = {Functional and Logic Programming}, |
|
117 series = {Lecture Notes in Computer Science}, |
|
118 editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán}, |
|
119 publisher = {Springer Berlin / Heidelberg}, |
|
120 isbn = {978-3-642-12250-7}, |
|
121 keyword = {Computer Science}, |
|
122 pages = {103-117}, |
|
123 volume = {6009}, |
|
124 url = {http://dx.doi.org/10.1007/978-3-642-12251-4\_9}, |
|
125 doi = {10.1007/978-3-642-12251-4\_9}, |
|
126 year = {2010} |
|
127 } |
|
128 @misc{url-afp, |
|
129 title = {Archive of {F}ormal {P}roofs}, |
|
130 howpublished = {\url{http://afp.sourceforge.net}} |
|
131 } |
|
132 @incollection {Cogent-to-C-2016, |
|
133 author = {S. Amani and A. Hixon and Z. Chen and C. Rizkallah and P. Chubb and L. O’Connor and |
|
134 J. Beeren and Y. Nagashima and J. Lim and T. Sewell and J. Tuong and G. Keller and T. Murray and |
|
135 G. Klein and G. Heiser}, |
|
136 title = {Cogent: Verifying High-Assurance File System Implementations}, |
|
137 booktitle = {International Conference on Architectural Support for Programming Languages and |
|
138 Operating Systems}, |
|
139 publisher = {Springer Berlin / Heidelberg}, |
|
140 address = {Atlanta, GA, USA}, |
|
141 pages = {175-188}, |
|
142 doi = {10.1145/2872362.2872404}, |
|
143 year = {2016} |
|
144 } |
|
145 @InProceedings{wn:proto-sys, |
|
146 author = {Krempler, Alan and Neuper, Walther}, |
|
147 year = {2018}, |
|
148 title = {Prototyping ``Systems that Explain Themselves'' for Education}, |
|
149 editor = {Quaresma, Pedro and Neuper, Walther}, |
|
150 booktitle = {{\rm Proceedings 6th International Workshop on} |
|
151 Theorem proving components for Educational software, |
|
152 {\rm Gothenburg, Sweden, 6 Aug 2017}}, |
|
153 series = {Electronic Proceedings in Theoretical Computer Science}, |
|
154 volume = {267}, |
|
155 publisher = {Open Publishing Association}, |
|
156 pages = {89-107}, |
|
157 doi = {10.4204/EPTCS.267.6} |
|
158 } |
|
159 @Book{Isa-tutor08, |
|
160 author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus}, |
|
161 title = {Isabelle/HOL, a proof assistant for high-order logic}, |
|
162 publisher = {Springer Verlag}, |
|
163 year = {2008} |
|
164 } |
|
165 @InCollection{pl:formal-lang-hist, |
|
166 author = {Lucas, Peter}, |
|
167 title = {On the Formalization of Programming Languages: Early History and Main Approaches}, |
|
168 booktitle = {The Vienna Development Method: The Meta-Language}, |
|
169 publisher = {Springer}, |
|
170 year = {1978}, |
|
171 editor = {D. Bj{\o}rner and C. B. Jones}, |
|
172 volume = {16}, |
|
173 series = {LNCS}, |
|
174 doi = {10.1007/3-540-08766-4\_8} |
|
175 } |
|
176 @InProceedings{thedu16:lucin-user-view, |
|
177 author = {Neuper, Walther}, |
|
178 title = {Lucas-Interpretation from Users' Perspective}, |
|
179 booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, |
|
180 and Work in Progress at the Conference on Intelligent Computer Mathematics}, |
|
181 year = {2016}, |
|
182 address = {Bialystok, Poland}, |
|
183 month = {July 25-29}, |
|
184 pages = {83-89}, |
|
185 note = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}} |
|
186 } |
|
187 @Misc{wn:lucin-thedu18, |
|
188 author = {Walther Neuper}, |
|
189 title = {Lucas-Interpretation from Programmers' Perspective}, |
|
190 year = {2018}, |
|
191 note = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}} |
|
192 } |
|
193 @InProceedings{wn:lucas-interp-12, |
|
194 author = "Neuper, Walther", |
|
195 year = "2012", |
|
196 title = "Automated Generation of User Guidance by Combining Computation and Deduction", |
|
197 pages = "82-101", |
|
198 doi = "10.4204/EPTCS.79.5", |
|
199 booktitle = {Electronic Proceedings in Theoretical Computer Science}, |
|
200 editor = "Quaresma, Pedro and Back, Ralph-Johan", |
|
201 volume = "79", |
|
202 publisher = "Open Publishing Association" |
|
203 } |
|
204 @Book{progr-mathematica-2012, |
|
205 author = {Maeder, Roman E.}, |
|
206 title = {Programming in Mathematica}, |
|
207 publisher = {Addison-Wesley}, |
|
208 address = {Reading, Mass.}, |
|
209 year = {2012}, |
|
210 edition = {3rd} |
|
211 } |
|
212 @PhdThesis{wn:diss, |
|
213 author = {Neuper, Walther }, |
|
214 title = {Reactive User-Guidance by an Autonomous Engine Doing High-School Math}, |
|
215 school = {IICM - Inst. f. Softwaretechnology}, |
|
216 year = {2001}, |
|
217 address = {Technical University, A-8010 Graz}, |
|
218 note = {\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}} |
|
219 } |
|
220 @Article{plmms10, |
|
221 author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper}, |
|
222 title = {{CTP}-based programming languages~? {C}onsiderations about an experimental design}, |
|
223 journal = {ACM Communications in Computer Algebra}, |
|
224 doi = {10.1145/1838599.1838621}, |
|
225 year = {2010}, |
|
226 volume = {44}, |
|
227 number = {1/2}, |
|
228 pages = {27-41}, |
|
229 month = {March/June} |
|
230 } |
|
231 @Article{back-SD-2010, |
|
232 author = {R.-J. Back}, |
|
233 title = {Structured derivations: a unified proof style for teaching mathematics}, |
|
234 journal = {Formal Aspects of Computing}, |
|
235 year = {2010}, |
|
236 volume = {22}, |
|
237 number = {5}, |
|
238 pages = {629-661} |
|
239 } |
|
240 @MastersThesis{mlehnf:bakk-11, |
|
241 author = {Mathias Lehnfeld}, |
|
242 title = {Verbindung von 'Computation' und 'Deduction' im \sisac-System}, |
|
243 school = {Institut f\"ur Computersprachen, Technische Universit\"at Wien}, |
|
244 year = {2011}, |
|
245 note = {Bakkalaureate project} |
|
246 } |
|
247 @incollection{paulson700, |
|
248 author = {Lawrence C. Paulson}, |
|
249 title = {{Isabelle}: The Next 700 Theorem Provers}, |
|
250 booktitle = {Logic and Computer Science}, |
|
251 editor = {P. Odifreddi}, |
|
252 pages = {361-386}, |
|
253 publisher = {Academic Press}, |
|
254 url = {https://arxiv.org/abs/cs/9301106}, |
|
255 year = {1990} |
|
256 } |
|
257 @misc{RISC4777, |
|
258 author = {B. Buchberger}, |
|
259 title = {{The Role of Mathematical Thinking for 21st Century Society}}, |
|
260 language = {english}, |
|
261 year = {2013}, |
|
262 month = {March 4-6}, |
|
263 annote = {2013-03-04-A}, |
|
264 note = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education}, |
|
265 institution = {Khemarak University, Phnom Penh, Cambodia}, |
|
266 conferencename = {The 2nd International Conference on Mathematics and Technology in Mathematics Education} |
|
267 } |
|
268 @Article{EMS-math-ethics, |
|
269 author = {Chiodo, Maurice and Clifton, Toby}, |
|
270 title = {The Importance of Ethics in Mathematics}, |
|
271 journal = {Newsletter of the European Mathematical Society}, |
|
272 year = {2019}, |
|
273 volume = {114}, |
|
274 pages = {34-37}, |
|
275 month = {December}, |
|
276 url = {\url{https://euro-math-soc.eu/newsletter}} |
|
277 } |
|
278 @MastersThesis{ggt02, |
|
279 author = {Karnel, Stefan}, |
|
280 title = {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \isac-Projekt}, |
|
281 school = {University of Technology, Institute of Mathematics}, |
|
282 year = {2002}, |
|
283 address = {Graz, Austria}, |
|
284 month = {Aug} |
|
285 } |
|
286 @InProceedings{gdaroczy-EP-13, |
|
287 author = {Gabriella Dar\'{o}czy and Walther Neuper}, |
|
288 title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems}, |
|
289 booktitle = {eJMT, the Electronic Journal of Mathematics \& Technology}, |
|
290 year = {2013}, |
|
291 volume = {7}, |
|
292 pages = {175-194}, |
|
293 month = {February}, |
|
294 note = {Special Issue ``TP-based Systems and Education''}, |
|
295 url = {\url{https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}} |
|
296 } |
|
297 @TECHREPORT{tBaBoEr07a, |
|
298 author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes}, |
|
299 title = {MathEdit: Tool Support for Structured Calculational Proofs}, |
|
300 institution = {TUCS}, |
|
301 year = {2007}, |
|
302 number = {854}, |
|
303 month = {Dec}, |
|
304 note = {\url{http://tucs.fi/publications/view/?pub_id=tBaBoEr07a}} |
|
305 } |
|
306 @article{Farmer_al:93, |
|
307 author = {W. D. Farmer and J. D. Guttman and F. J. Thayer}, |
|
308 title = {{IMPS: An Interactive Mathematical Proof System}}, |
|
309 journal = {Journal of Automated Reasoning}, |
|
310 year = {1993}, |
|
311 volume = {11}, |
|
312 month = {August}, |
|
313 number = {2}, |
|
314 pages = {213-248}, |
|
315 } |
|
316 @InProceedings{gclc-06, |
|
317 author = {Jani\v{c}i\'c, Predrag}, |
|
318 title = {{GCLC} --- a tool for constructive euclidean geometry and more than that}, |
|
319 booktitle = {Mathematical Software -- {ICMS} 2006}, |
|
320 pages = {58-73}, |
|
321 year = {2006}, |
|
322 number = {4151} |
|
323 } |
|
324 @Article{ggb:atp-15, |
|
325 author = {Botana, F. and Hohenwarter, M. and Jani\v{c}i\'c, P. and Kov\'acs, Z. and Petrovi\'c, I. and Recio, T. and Weitzhofer, S.}, |
|
326 title = {Automated Theorem Proving in {GeoGebra}: Current Achievements}, |
|
327 journal = {Journal of Automated Reasoning}, |
|
328 year = {2015}, |
|
329 volume = {55}, |
|
330 number = {1}, |
|
331 pages = {39-59}, |
|
332 ISSN = {0168-7433}, |
|
333 DOI = {http://dx.doi.org/10.1007/s10817-015-9326-4} |
|
334 } |
|
335 @Manual{isabelle-jedit, |
|
336 title = {{Isabelle/jEdit}}, |
|
337 author = {Makarius Wenzel}, |
|
338 address = {Munich}, |
|
339 note = {Part of the Isabelle distribution}, |
|
340 note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}} |
|
341 } |
|
342 @TechReport{Yacc-1975, |
|
343 author = {Johnson, Stephen C.}, |
|
344 title = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler}, |
|
345 institution = {AT\&T Bell Laboratories}, |
|
346 year = {1975}, |
|
347 number = {32}, |
|
348 address = {Murray Hill, New Jersey}, |
|
349 note = {Retrieved 31 January 2020} |
|
350 } |
|
351 |