1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.bib Wed Mar 11 15:25:52 2020 +0100
1.3 @@ -0,0 +1,351 @@
1.4 +
1.5 +@Proceedings{EPTCS79,
1.6 + title = {{\rm Proceedings First Workshop on}
1.7 + CTP Components for Educational Software (THedu'11)},
1.8 + year = {2012},
1.9 + booktitle = {Electronic Proceedings in Theoretical Computer Science},
1.10 + editor = "Quaresma, Pedro and Back, Ralph-Johan",
1.11 + volume = "79",
1.12 + publisher = "Open Publishing Association"
1.13 +}
1.14 +@techreport{RISC5885,
1.15 +author = {David M. Cerna},
1.16 +title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
1.17 +year = {2019},
1.18 +month = {Feburary},
1.19 +length = {17},
1.20 +type = {RISC Report Series},
1.21 +institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
1.22 +address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
1.23 +}
1.24 +@Article{EMS-STT-19,
1.25 + author = {Koichu, Boris and Pinto, Alon},
1.26 + title = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?},
1.27 + journal = {EMS Newsletter},
1.28 + year = {2019},
1.29 + pages = {34-35},
1.30 + month = {June},
1.31 + doi = {10.4171/NEWS}
1.32 +}
1.33 +
1.34 +@Inproceedings{EPTCS290.6,
1.35 + author = {Neuper, Walther},
1.36 + year = {2019},
1.37 + title = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education},
1.38 + editor = {Quaresma, Pedro and Neuper, Walther},
1.39 + booktitle = {{\rm Proceedings 7th International Workshop on}
1.40 + Theorem proving components for Educational software,
1.41 + {\rm Oxford, United Kingdom, 18 july 2018}},
1.42 + series = {Electronic Proceedings in Theoretical Computer Science},
1.43 + volume = {290},
1.44 + publisher = {Open Publishing Association},
1.45 + pages = {76-95},
1.46 + doi = {10.4204/EPTCS.290.6}
1.47 +}
1.48 +@InProceedings{wneuper:gcd-coimbra,
1.49 + author = {Neuper, Walther},
1.50 + title = {{GCD} --- A Case Study on {L}ucas-Interpretation},
1.51 + booktitle = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM},
1.52 + year = {2014},
1.53 + address = {Coimbra, Portugal},
1.54 + month = {July 7-11},
1.55 + note = {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}}
1.56 +}
1.57 +@Article{flip-class-meta,
1.58 + author = {Shi, Y. and Ma, Y. and MacLeod, J. and others},
1.59 + title = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature},
1.60 + journal = {Journal of Computers in Education},
1.61 + year = {2019},
1.62 + pages = {1-25},
1.63 + month = {May},
1.64 + doi = {https://doi.org/10.1007/s40692-019-00142-8}
1.65 +}
1.66 +@inproceedings{krauss,
1.67 + author = {Krauss, Alexander},
1.68 + title = {Partial Recursive Functions in Higher-Order Logic},
1.69 + pages = {589-603},
1.70 + doi = {10.1007/11814771\_48},
1.71 + editor = {Ulrich Furbach and Natarajan Shankar},
1.72 + booktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006},
1.73 + publisher = {Springer},
1.74 + series = {Lecture Notes in Computer Science},
1.75 + volume = {4130},
1.76 + year = {2006},
1.77 + bibsource = {DBLP, http://dblp.uni-trier.de}
1.78 +}
1.79 +@Manual{funpack-tutorial,
1.80 + title = {Defining Recursive Functions in {Isabelle/HOL}},
1.81 + author = {Alexander Krauss},
1.82 + address = {Munich},
1.83 + year = {},
1.84 + note = {{P}art of the Isabelle distribution},
1.85 + url = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
1.86 +}
1.87 +@Misc{nipkow-prog-prove-ny,
1.88 + author = {Nipkow, Tobias},
1.89 + title = {Programming and Proving in {Isabelle/HOL}},
1.90 + howpublished = {contained in the Isabelle distribution},
1.91 + year = {},
1.92 + url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
1.93 +}
1.94 +@Misc{code-gen-tutorial,
1.95 + author = {Florian Haftmann},
1.96 + title = {Code generation from {Isabelle/HOL} theories},
1.97 + howpublished = {Contained in the Isabelle distribution},
1.98 + year = {},
1.99 + url = {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}
1.100 +}
1.101 +@Misc{implem-tutorial,
1.102 + author = {Makarius Wenzel},
1.103 + title = {The {Isabelle/Isar} Implementation},
1.104 + howpublished = {Contained in the Isabelle distribution},
1.105 + year = {},
1.106 + url = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}
1.107 +}
1.108 +@Misc{sledgehammer-tutorial,
1.109 + author = {Jasmin C.Blanchette},
1.110 + title = {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}},
1.111 + howpublished = {contained in the Isabelle distribution},
1.112 + year = {},
1.113 + url = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}
1.114 +}
1.115 +@incollection {haftm-nipkow-code-gen-HRS-10,
1.116 + author = {Haftmann, Florian and Nipkow, Tobias},
1.117 + affiliation = {Institut für Informatik, Technische Universität München},
1.118 + title = {Code Generation via Higher-Order Rewrite Systems},
1.119 + booktitle = {Functional and Logic Programming},
1.120 + series = {Lecture Notes in Computer Science},
1.121 + editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán},
1.122 + publisher = {Springer Berlin / Heidelberg},
1.123 + isbn = {978-3-642-12250-7},
1.124 + keyword = {Computer Science},
1.125 + pages = {103-117},
1.126 + volume = {6009},
1.127 + url = {http://dx.doi.org/10.1007/978-3-642-12251-4\_9},
1.128 + doi = {10.1007/978-3-642-12251-4\_9},
1.129 + year = {2010}
1.130 +}
1.131 +@misc{url-afp,
1.132 + title = {Archive of {F}ormal {P}roofs},
1.133 + howpublished = {\url{http://afp.sourceforge.net}}
1.134 +}
1.135 +@incollection {Cogent-to-C-2016,
1.136 + author = {S. Amani and A. Hixon and Z. Chen and C. Rizkallah and P. Chubb and L. O’Connor and
1.137 +J. Beeren and Y. Nagashima and J. Lim and T. Sewell and J. Tuong and G. Keller and T. Murray and
1.138 +G. Klein and G. Heiser},
1.139 + title = {Cogent: Verifying High-Assurance File System Implementations},
1.140 + booktitle = {International Conference on Architectural Support for Programming Languages and
1.141 +Operating Systems},
1.142 + publisher = {Springer Berlin / Heidelberg},
1.143 + address = {Atlanta, GA, USA},
1.144 + pages = {175-188},
1.145 + doi = {10.1145/2872362.2872404},
1.146 + year = {2016}
1.147 +}
1.148 +@InProceedings{wn:proto-sys,
1.149 + author = {Krempler, Alan and Neuper, Walther},
1.150 + year = {2018},
1.151 + title = {Prototyping ``Systems that Explain Themselves'' for Education},
1.152 + editor = {Quaresma, Pedro and Neuper, Walther},
1.153 + booktitle = {{\rm Proceedings 6th International Workshop on}
1.154 + Theorem proving components for Educational software,
1.155 + {\rm Gothenburg, Sweden, 6 Aug 2017}},
1.156 + series = {Electronic Proceedings in Theoretical Computer Science},
1.157 + volume = {267},
1.158 + publisher = {Open Publishing Association},
1.159 + pages = {89-107},
1.160 + doi = {10.4204/EPTCS.267.6}
1.161 +}
1.162 +@Book{Isa-tutor08,
1.163 + author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
1.164 + title = {Isabelle/HOL, a proof assistant for high-order logic},
1.165 + publisher = {Springer Verlag},
1.166 + year = {2008}
1.167 +}
1.168 +@InCollection{pl:formal-lang-hist,
1.169 + author = {Lucas, Peter},
1.170 + title = {On the Formalization of Programming Languages: Early History and Main Approaches},
1.171 + booktitle = {The Vienna Development Method: The Meta-Language},
1.172 + publisher = {Springer},
1.173 + year = {1978},
1.174 + editor = {D. Bj{\o}rner and C. B. Jones},
1.175 + volume = {16},
1.176 + series = {LNCS},
1.177 + doi = {10.1007/3-540-08766-4\_8}
1.178 +}
1.179 +@InProceedings{thedu16:lucin-user-view,
1.180 + author = {Neuper, Walther},
1.181 + title = {Lucas-Interpretation from Users' Perspective},
1.182 + booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program,
1.183 +and Work in Progress at the Conference on Intelligent Computer Mathematics},
1.184 + year = {2016},
1.185 + address = {Bialystok, Poland},
1.186 + month = {July 25-29},
1.187 + pages = {83-89},
1.188 + note = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}}
1.189 +}
1.190 +@Misc{wn:lucin-thedu18,
1.191 + author = {Walther Neuper},
1.192 + title = {Lucas-Interpretation from Programmers' Perspective},
1.193 + year = {2018},
1.194 + note = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}}
1.195 +}
1.196 +@InProceedings{wn:lucas-interp-12,
1.197 + author = "Neuper, Walther",
1.198 + year = "2012",
1.199 + title = "Automated Generation of User Guidance by Combining Computation and Deduction",
1.200 + pages = "82-101",
1.201 + doi = "10.4204/EPTCS.79.5",
1.202 + booktitle = {Electronic Proceedings in Theoretical Computer Science},
1.203 + editor = "Quaresma, Pedro and Back, Ralph-Johan",
1.204 + volume = "79",
1.205 + publisher = "Open Publishing Association"
1.206 +}
1.207 +@Book{progr-mathematica-2012,
1.208 + author = {Maeder, Roman E.},
1.209 + title = {Programming in Mathematica},
1.210 + publisher = {Addison-Wesley},
1.211 + address = {Reading, Mass.},
1.212 + year = {2012},
1.213 + edition = {3rd}
1.214 +}
1.215 +@PhdThesis{wn:diss,
1.216 + author = {Neuper, Walther },
1.217 + title = {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
1.218 + school = {IICM - Inst. f. Softwaretechnology},
1.219 + year = {2001},
1.220 + address = {Technical University, A-8010 Graz},
1.221 + note = {\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}}
1.222 +}
1.223 +@Article{plmms10,
1.224 + author = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
1.225 + title = {{CTP}-based programming languages~? {C}onsiderations about an experimental design},
1.226 + journal = {ACM Communications in Computer Algebra},
1.227 + doi = {10.1145/1838599.1838621},
1.228 + year = {2010},
1.229 + volume = {44},
1.230 + number = {1/2},
1.231 + pages = {27-41},
1.232 + month = {March/June}
1.233 +}
1.234 +@Article{back-SD-2010,
1.235 + author = {R.-J. Back},
1.236 + title = {Structured derivations: a unified proof style for teaching mathematics},
1.237 + journal = {Formal Aspects of Computing},
1.238 + year = {2010},
1.239 + volume = {22},
1.240 + number = {5},
1.241 + pages = {629-661}
1.242 +}
1.243 +@MastersThesis{mlehnf:bakk-11,
1.244 + author = {Mathias Lehnfeld},
1.245 + title = {Verbindung von 'Computation' und 'Deduction' im \sisac-System},
1.246 + school = {Institut f\"ur Computersprachen, Technische Universit\"at Wien},
1.247 + year = {2011},
1.248 + note = {Bakkalaureate project}
1.249 +}
1.250 +@incollection{paulson700,
1.251 + author = {Lawrence C. Paulson},
1.252 + title = {{Isabelle}: The Next 700 Theorem Provers},
1.253 + booktitle = {Logic and Computer Science},
1.254 + editor = {P. Odifreddi},
1.255 + pages = {361-386},
1.256 + publisher = {Academic Press},
1.257 + url = {https://arxiv.org/abs/cs/9301106},
1.258 + year = {1990}
1.259 +}
1.260 +@misc{RISC4777,
1.261 + author = {B. Buchberger},
1.262 + title = {{The Role of Mathematical Thinking for 21st Century Society}},
1.263 + language = {english},
1.264 + year = {2013},
1.265 + month = {March 4-6},
1.266 + annote = {2013-03-04-A},
1.267 + note = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education},
1.268 + institution = {Khemarak University, Phnom Penh, Cambodia},
1.269 + conferencename = {The 2nd International Conference on Mathematics and Technology in Mathematics Education}
1.270 +}
1.271 +@Article{EMS-math-ethics,
1.272 + author = {Chiodo, Maurice and Clifton, Toby},
1.273 + title = {The Importance of Ethics in Mathematics},
1.274 + journal = {Newsletter of the European Mathematical Society},
1.275 + year = {2019},
1.276 + volume = {114},
1.277 + pages = {34-37},
1.278 + month = {December},
1.279 + url = {\url{https://euro-math-soc.eu/newsletter}}
1.280 +}
1.281 +@MastersThesis{ggt02,
1.282 + author = {Karnel, Stefan},
1.283 + title = {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \isac-Projekt},
1.284 + school = {University of Technology, Institute of Mathematics},
1.285 + year = {2002},
1.286 + address = {Graz, Austria},
1.287 + month = {Aug}
1.288 +}
1.289 +@InProceedings{gdaroczy-EP-13,
1.290 + author = {Gabriella Dar\'{o}czy and Walther Neuper},
1.291 + title = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
1.292 + booktitle = {eJMT, the Electronic Journal of Mathematics \& Technology},
1.293 + year = {2013},
1.294 + volume = {7},
1.295 + pages = {175-194},
1.296 + month = {February},
1.297 + note = {Special Issue ``TP-based Systems and Education''},
1.298 + url = {\url{https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}}
1.299 +}
1.300 +@TECHREPORT{tBaBoEr07a,
1.301 + author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes},
1.302 + title = {MathEdit: Tool Support for Structured Calculational Proofs},
1.303 + institution = {TUCS},
1.304 + year = {2007},
1.305 + number = {854},
1.306 + month = {Dec},
1.307 + note = {\url{http://tucs.fi/publications/view/?pub_id=tBaBoEr07a}}
1.308 +}
1.309 +@article{Farmer_al:93,
1.310 +author = {W. D. Farmer and J. D. Guttman and F. J. Thayer},
1.311 +title = {{IMPS: An Interactive Mathematical Proof System}},
1.312 +journal = {Journal of Automated Reasoning},
1.313 +year = {1993},
1.314 +volume = {11},
1.315 +month = {August},
1.316 +number = {2},
1.317 +pages = {213-248},
1.318 +}
1.319 +@InProceedings{gclc-06,
1.320 + author = {Jani\v{c}i\'c, Predrag},
1.321 + title = {{GCLC} --- a tool for constructive euclidean geometry and more than that},
1.322 + booktitle = {Mathematical Software -- {ICMS} 2006},
1.323 + pages = {58-73},
1.324 + year = {2006},
1.325 + number = {4151}
1.326 +}
1.327 +@Article{ggb:atp-15,
1.328 + 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.},
1.329 + title = {Automated Theorem Proving in {GeoGebra}: Current Achievements},
1.330 + journal = {Journal of Automated Reasoning},
1.331 + year = {2015},
1.332 + volume = {55},
1.333 + number = {1},
1.334 + pages = {39-59},
1.335 + ISSN = {0168-7433},
1.336 + DOI = {http://dx.doi.org/10.1007/s10817-015-9326-4}
1.337 +}
1.338 +@Manual{isabelle-jedit,
1.339 + title = {{Isabelle/jEdit}},
1.340 + author = {Makarius Wenzel},
1.341 + address = {Munich},
1.342 + note = {Part of the Isabelle distribution},
1.343 + note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}
1.344 +}
1.345 +@TechReport{Yacc-1975,
1.346 + author = {Johnson, Stephen C.},
1.347 + title = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler},
1.348 + institution = {AT\&T Bell Laboratories},
1.349 + year = {1975},
1.350 + number = {32},
1.351 + address = {Murray Hill, New Jersey},
1.352 + note = {Retrieved 31 January 2020}
1.353 +}
1.354 +