@misc(url-afp,
 title        = {Archive of {F}ormal {P}roofs},
 howpublished = {\url{http://afp.sourceforge.net}},
)
@incollection(Cogent-to-C-2016,
 author       = {S. Amani and A. Hixon and Z. Chen and C. Rizkallah and P. Chubb and L. O’Connor and J. Beeren and Y. Nagashima and J. Lim and T. Sewell and J. Tuong and G. Keller and T. Murray and G. Klein and G. Heiser},
 year         = {2016},
 title        = {Cogent: Verifying High-Assurance File System Implementations},
 booktitle    = {International Conference on Architectural Support for Programming Languages and Operating Systems},
 publisher    = {Springer Berlin / Heidelberg},
 address      = {Atlanta, GA, USA},
 pages        = {175--188},
 doi          = {10.1145/2872362.2872404},
)
@article(back-SD-2010,
 author       = {R.-J. Back},
 year         = {2010},
 title        = {Structured derivations: a unified proof style for teaching mathematics},
 journal      = {Formal Aspects of Computing},
 volume       = {22},
 number       = {5},
 pages        = {629--661},
 doi          = {10.1007/s00165-009-0136-5},
)
@techreport(tBaBoEr07a,
 author       = {Ralph-Johan Back and Victor Bos and Johannes Eriksson},
 year         = {2007},
 title        = {MathEdit: Tool Support for Structured Calculational Proofs},
 type         = {Technical Report},
 number       = {854},
 institution  = {TUCS},
 url          = {http://tucs.fi/publications/view/?pub_id=tBaBoEr07a},
)
@article(ggb:atp-15,
 author       = {F. Botana and M. Hohenwarter and Jani\v{c}i\'c, P. and Z. Kov\'acs and I. Petrovi\'c and T. Recio and S. Weitzhofer},
 year         = {2015},
 title        = {Automated Theorem Proving in {GeoGebra}: Current Achievements},
 journal      = {Journal of Automated Reasoning},
 volume       = {55},
 number       = {1},
 pages        = {39--59},
 doi          = {10.1007/s10817-015-9326-4},
)
@misc(RISC4777,
 author       = {B. Buchberger},
 year         = {2013},
 title        = {{The Role of Mathematical Thinking for 21st Century Society}},
 note         = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education},
)
@misc(sledgehammer-tutorial,
 author       = {Jasmin C.Blanchette},
 title        = {{Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL}},
 howpublished = {contained in the Isabelle distribution},
 url          = {http://isabelle.in.tum.de/doc/sledgehammer.pdf},
)
@techreport(RISC5885,
 author       = {David M. Cerna},
 year         = {2019},
 title        = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
 type         = {RISC Report Series},
 institution  = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
 address      = {Schloss Hagenberg, 4232 Hagenberg, Austria},
)
@article(EMS-math-ethics,
 author       = {Maurice Chiodo and Toby Clifton},
 year         = {2019},
 title        = {The Importance of Ethics in Mathematics},
 journal      = {Newsletter of the European Mathematical Society},
 volume       = {114},
 pages        = {34--37},
 doi          = {10.4171/NEWS/114/9},
)
@inproceedings(gdaroczy-EP-13,
 author       = {Gabriella Dar\'{o}czy and Walther Neuper},
 year         = {2013},
 title        = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
 booktitle    = {eJMT, the Electronic Journal of Mathematics \& Technology},
 volume       = {7},
 pages        = {175--194},
 url          = {https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2},
 note         = {Special Issue ``TP-based Systems and Education''},
)
@article(Farmer-al:93,
 author       = {W. D. Farmer and J. D. Guttman and F. J. Thayer},
 year         = {1993},
 title        = {{IMPS: An Interactive Mathematical Proof System}},
 journal      = {Journal of Automated Reasoning},
 volume       = {11},
 number       = {2},
 pages        = {213--248},
 doi          = {10.1007/BF00881906},
)
@misc(code-gen-tutorial,
 author       = {Florian Haftmann},
 title        = {Code generation from {Isabelle/HOL} theories},
 howpublished = {Contained in the Isabelle distribution},
 url          = {http://isabelle.in.tum.de/doc/prog-prove.pdf},
)
@article(plmms10,
 author       = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
 year         = {2010},
 title        = {{CTP}-based programming languages~? {C}onsiderations about an experimental design},
 journal      = {ACM Communications in Computer Algebra},
 volume       = {44},
 number       = {1/2},
 pages        = {27--41},
 doi          = {10.1145/1838599.1838621},
)
@incollection(haftm-nipkow-code-gen-HRS-10,
 author       = {Florian Haftmann and Tobias Nipkow},
 year         = {2010},
 title        = {Code Generation via Higher-Order Rewrite Systems},
 editor       = {Matthias Blume and Naoki Kobayashi and Germán Vidal},
 booktitle    = {Functional and Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {6009},
 publisher    = {Springer Berlin / Heidelberg},
 pages        = {103--117},
 doi          = {10.1007/978-3-642-12251-4\_9},
)
@inproceedings(gclc-06,
 author       = {Jani\v{c}i\'c, Predrag},
 year         = {2006},
 title        = {{GCLC} --- a tool for constructive euclidean geometry and more than that},
 booktitle    = {Mathematical Software -- {ICMS} 2006},
 volume       = {4151},
 pages        = {58--73},
 doi          = {10.1007/11812289_22},
)
@techreport(Yacc-1975,
 author       = {Stephen C. Johnson},
 year         = {1975},
 title        = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler},
 type         = {Technical Report},
 number       = {32},
 institution  = {AT\&T Bell Laboratories},
 address      = {Murray Hill, New Jersey},
 note         = {Retrieved 31 January 2020},
)
@mastersthesis(ggt02,
 author       = {Stefan Karnel},
 year         = {2002},
 title        = {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \textit{ISAC}-Projekt},
 school       = {University of Technology, Institute of Mathematics},
 address      = {Graz, Austria},
 url          = {https://static.miraheze.org/isacwiki/3/3e/GGTs-von-Polynomen.pdf},
)
@mastersthesis(mkienl-bakk,
 author       = {Markus Kienleitner},
 year         = {2012},
 title        = {Towards ``NextStep Userguidance'' in a Mechanized Math Assistant},
 school       = {IICM, Graz University of Technology},
 url          = {https://static.miraheze.org/isacwiki/0/0d/Mkienl_bakk.pdf},
)
@article(EMS-STT-19,
 author       = {Boris Koichu and Alon Pinto},
 year         = {2019},
 title        = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?},
 journal      = {EMS Newsletter},
 pages        = {34--35},
 doi          = {10.4171/NEWS},
)
@manual(funpack-tutorial,
 author       = {Alexander Krauss},
 title        = {Defining Recursive Functions in {Isabelle/HOL}},
 address      = {Munich},
 url          = {http://isabelle.in.tum.de/doc/functions.pdf},
 note         = {{P}art of the {I}sabelle distribution},
)
@inproceedings(krauss,
 author       = {Alexander Krauss},
 year         = {2006},
 title        = {Partial Recursive Functions in Higher-Order Logic},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated Reasoning, Third International Joint Conference, IJCAR 2006},
 series       = {Lecture Notes in Computer Science},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {589--603},
 doi          = {10.1007/11814771\_48},
)
@inproceedings(wn:proto-sys,
 author       = {Alan Krempler and Walther Neuper},
 year         = {2018},
 title        = {Prototyping ``Systems that Explain Themselves'' for Education},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 6th International Workshop on} Theorem proving components for Educational software, {\rm Gothenburg, Sweden, 6 Aug 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {267},
 publisher    = {Open Publishing Association},
 pages        = {89--107},
 doi          = {10.4204/EPTCS.267.6},
)
@mastersthesis(mlehnf:bakk-11,
 author       = {Mathias Lehnfeld},
 year         = {2011},
 title        = {Verbindung von 'Computation' und 'Deduction' im \textit{ISAC}-System},
 school       = {Institut f\"ur Computersprachen, Technische Universit\"at Wien},
 note         = {Bakkalaureate project},
)
@incollection(pl:formal-lang-hist,
 author       = {Peter Lucas},
 year         = {1978},
 title        = {On the Formalization of Programming Languages: Early History and Main Approaches},
 editor       = {Bj{\o}rner, D. and C. B. Jones},
 booktitle    = {The Vienna Development Method: The Meta-Language},
 series       = {LNCS},
 volume       = {16},
 publisher    = {Springer},
 doi          = {10.1007/3-540-08766-4\_8},
)
@book(progr-mathematica-2012,
 author       = {Roman E. Maeder},
 year         = {2012},
 title        = {Programming in Mathematica},
 edition      = {3rd},
 publisher    = {Addison-Wesley},
 address      = {Reading, Mass.},
)
@phdthesis(wn:diss,
 author       = {Walther Neuper},
 year         = {2001},
 title        = {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},
 school       = {IICM - Inst. f. Softwaretechnology},
 address      = {Technical University, A-8010 Graz},
 url          = {https://static.miraheze.org/isacwiki/8/8a/Wn-diss.pdf},
)
@inproceedings(wn:lucas-interp-12,
 author       = {Walther Neuper},
 year         = {2012},
 title        = {Automated Generation of User Guidance by Combining Computation and Deduction},
 editor       = {Pedro Quaresma and Ralph-Johan Back},
 booktitle    = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {79},
 publisher    = {Open Publishing Association},
 pages        = {82--101},
 doi          = {10.4204/EPTCS.79.5},
)
@inproceedings(wneuper:gcd-coimbra,
 author       = {Walther Neuper},
 year         = {2014},
 title        = {{GCD} --- A Case Study on {L}ucas-Interpretation},
 booktitle    = {Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM},
 address      = {Coimbra, Portugal},
 url          = {http://ceur-ws.org/Vol-1186/paper-17.pdf},
 note         = {Urn:nbn:de:0074-1186-1},
)
@inproceedings(thedu16:lucin-user-view,
 author       = {Walther Neuper},
 year         = {2016},
 title        = {Lucas-Interpretation from Users' Perspective},
 booktitle    = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics},
 address      = {Bialystok, Poland},
 pages        = {83--89},
 url          = {http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf},
 note         = {Urn:nbn:de:0074-1785-8},
)
@misc(wn:lucin-thedu18,
 author       = {Walther Neuper},
 year         = {2018},
 title        = {Lucas-Interpretation from Programmers' Perspective},
 url          = {https://static.miraheze.org/isacwiki/8/83/Lucin-prog-view.pdf},
 note         = {Abstract for ThEdu'18},
)
@inproceedings(wn:cme-ei-18,
 author       = {Walther Neuper},
 year         = {2018},
 title        = {Mechanical Explanation in ``Systems that explain themselves''},
 editor       = {Osman Hasan},
 booktitle    = {Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018},
 publisher    = {Conference on Intelligent Computer Mathematics CICM},
 address      = {Hagenberg, Austria},
 url          = {https://www.cicm-conference.org/2018/infproc/paper1.pdf},
 note         = {Urn:nbn:de:0074-2307-7},
)
@inproceedings(EPTCS290.6,
 author       = {Walther Neuper},
 year         = {2019},
 title        = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 7th International Workshop on} Theorem proving components for Educational software, {\rm Oxford, United Kingdom, 18 july 2018}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {290},
 publisher    = {Open Publishing Association},
 pages        = {76--95},
 doi          = {10.4204/EPTCS.290.6},
)
@techreport(imst-htl07,
 author       = {Walther Neuper and Christian D\"urnsteiner},
 year         = {2007},
 title        = {{Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software}},
 type         = {Technical Report},
 number       = {683},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 url          = {https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf},
)
@techreport(imst-hpts08,
 author       = {Walther Neuper and Johannes Reitinger and Angelika Gr\"undlinger},
 year         = {2008},
 title        = {{Begreifen und Mechanisieren beim Algebra Einstieg}},
 type         = {Technical Report},
 number       = {1063},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 url          = {https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf},
)
@techreport(imst-htl06,
 author       = {Walther Neuper},
 year         = {2006},
 title        = {{Angewandte Mathematik und Fachtheorie}},
 type         = {Technical Report},
 number       = {357},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 url          = {http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte\_Mathematik\_und\_Fachtheorie},
)
@misc(nipkow-prog-prove-ny,
 author       = {Tobias Nipkow},
 title        = {Programming and Proving in {Isabelle/HOL}},
 howpublished = {contained in the Isabelle distribution},
 url          = {http://isabelle.in.tum.de/doc/prog-prove.pdf},
)
@book(Isa-tutor08,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2008},
 title        = {Isabelle/HOL, a proof assistant for high-order logic},
 publisher    = {Springer Verlag},
)
@incollection(paulson700,
 author       = {Lawrence C. Paulson},
 year         = {1990},
 title        = {{Isabelle}: The Next 700 Theorem Provers},
 editor       = {P. Odifreddi},
 booktitle    = {Logic and Computer Science},
 publisher    = {Academic Press},
 pages        = {361--386},
 url          = {https://arxiv.org/abs/cs/9301106},
)
@proceedings(EPTCS79,
 editor       = {Pedro Quaresma and Ralph-Johan Back},
 year         = {2012},
 title        = {{\rm Proceedings First Workshop on} CTP Components for Educational Software (THedu'11)},
 volume       = {79},
 publisher    = {Open Publishing Association},
 doi          = {10.4204/EPTCS.79},
)
@article(flip-class-meta,
 author       = {Y. Shi and Y. Ma and J. MacLeod},
 year         = {2019},
 title        = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature},
 journal      = {Journal of Computers in Education},
 pages        = {1--25},
 doi          = {10.1007/s40692-019-00142-8},
)
@misc(implem-tutorial,
 author       = {Makarius Wenzel},
 title        = {The {Isabelle/Isar} Implementation},
 howpublished = {Contained in the Isabelle distribution},
 url          = {http://isabelle.in.tum.de/doc/implementation.pdf},
)
@manual(isabelle-jedit,
 author       = {Makarius Wenzel},
 title        = {{Isabelle/jEdit}},
 address      = {Munich},
 url          = {http://isabelle.in.tum.de/doc/jedit.pdf},
 note         = {Part of the Isabelle distribution},
)
@inproceedings(DBLP:journals/corr/Wenzel14,
 author       = {Makarius Wenzel},
 year         = {2014},
 title        = {System description: {Isabelle/jEdit} in 2014},
 booktitle    = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July 2014.},
 pages        = {84--94},
 doi          = {10.4204/EPTCS.167.10},
)