@Proceedings{EPTCS79,

   title = 	 {{\rm Proceedings First Workshop on}

                CTP Components for Educational Software (THedu'11)},

   year = 	 {2012},

   booktitle = {Electronic Proceedings in Theoretical Computer Science},

   editor    = "Quaresma, Pedro and Back, Ralph-Johan",

   volume    = "79",

   publisher = "Open Publishing Association"

 }

 @techreport{RISC5885,

 author = {David M. Cerna},

 title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},

 year = {2019},

 month = {Feburary},

 length = {17},

 type = {RISC Report Series},

 institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

 address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

 }

 @Article{EMS-STT-19,

   author = {Koichu, Boris and Pinto, Alon},

   title = {The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?},

   journal = {EMS Newsletter},

   year = {2019},

   pages = {34-35},

   month = {June},

   doi = {10.4171/NEWS}

 }

 @Inproceedings{EPTCS290.6,

   author    = {Neuper, Walther},

   year      = {2019},

   title     = {Technologies for "Complete, Transparent \& Interactive Models of Math" in Education},

   editor    = {Quaresma, Pedro and Neuper, Walther},

   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}

 }

 @InProceedings{wneuper:gcd-coimbra,

   author = 	 {Neuper, Walther},

   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},

   year = 	 {2014},

   address = 	 {Coimbra, Portugal},

   month = 	 {July 7-11},

   note = 	 {\url{http://ceur-ws.org/Vol-1186/paper-17.pdf}}

 }

 @Article{flip-class-meta,

   author = {Shi, Y. and Ma, Y. and MacLeod, J. and others},

   title = {College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature},

   journal = {Journal of Computers in Education},

   year = {2019},

   pages = {1-25},

   month = {May},

   doi = {https://doi.org/10.1007/s40692-019-00142-8}

 }

 @inproceedings{krauss,

   author    = {Krauss, Alexander},

   title     = {Partial Recursive Functions in Higher-Order Logic},

   pages     = {589-603},

   doi       = {10.1007/11814771\_48},

   editor    = {Ulrich Furbach and Natarajan Shankar},

   booktitle     = {Automated Reasoning, Third International Joint Conference, IJCAR 2006},

   publisher = {Springer},

   series    = {Lecture Notes in Computer Science},

   volume    = {4130},

   year      = {2006},

   bibsource = {DBLP, http://dblp.uni-trier.de}

 }

 @Manual{funpack-tutorial,

   title = 	 {Defining Recursive Functions in {Isabelle/HOL}},

   author = 	 {Alexander Krauss},

   address = 	 {Munich},

   year = 	 {},

   note = 	 {{P}art of the Isabelle distribution},

   url = 	 {\url{http://isabelle.in.tum.de/doc/functions.pdf}}

 }

 @Misc{nipkow-prog-prove-ny,

   author = 	 {Nipkow, Tobias},

   title = 	 {Programming and Proving in {Isabelle/HOL}},

   howpublished = {contained in the Isabelle distribution},

   year = 	 {},

   url = 	 {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}

 }

 @Misc{code-gen-tutorial,

   author = 	 {Florian Haftmann},

   title = 	 {Code generation from {Isabelle/HOL} theories},

   howpublished = {Contained in the Isabelle distribution},

   year = 	 {},

   url = 	 {\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}

 }

 @Misc{implem-tutorial,

   author = 	 {Makarius Wenzel},

   title = 	 {The {Isabelle/Isar} Implementation},

   howpublished = {Contained in the Isabelle distribution},

   year = 	 {},

   url = 	 {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}

 }

 @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},

   year = 	 {},

   url = 	 {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}}

 }

 @incollection {haftm-nipkow-code-gen-HRS-10,

    author = {Haftmann, Florian and Nipkow, Tobias},

    affiliation = {Institut für Informatik, Technische Universität München},

    title = {Code Generation via Higher-Order Rewrite Systems},

    booktitle = {Functional and Logic Programming},

    series = {Lecture Notes in Computer Science},

    editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán},

    publisher = {Springer Berlin / Heidelberg},

    isbn = {978-3-642-12250-7},

    keyword = {Computer Science},

    pages = {103-117},

    volume = {6009},

    url = {http://dx.doi.org/10.1007/978-3-642-12251-4\_9},

    doi = {10.1007/978-3-642-12251-4\_9},

    year = {2010}

 }

 @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},

    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},

    year = {2016}

 }

 @InProceedings{wn:proto-sys,

   author    = {Krempler, Alan and Neuper, Walther},

   year      = {2018},

   title     = {Prototyping ``Systems that Explain Themselves'' for Education},

   editor    = {Quaresma, Pedro and Neuper, Walther},

   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}

 }

 @Book{Isa-tutor08,

   author = 	 {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},

   title = 	 {Isabelle/HOL, a proof assistant for high-order logic},

   publisher = 	 {Springer Verlag},

   year = 	 {2008}

 }

 @InCollection{pl:formal-lang-hist,

   author = 	 {Lucas, Peter},

   title = 	 {On the Formalization of Programming Languages: Early History and Main Approaches},

   booktitle = 	 {The Vienna Development Method: The Meta-Language},

   publisher = {Springer},

   year = 	 {1978},

   editor = 	 {D. Bj{\o}rner and C. B. Jones},

   volume = 	 {16},

   series = 	 {LNCS},

   doi = {10.1007/3-540-08766-4\_8}

 }

 @InProceedings{thedu16:lucin-user-view,

   author = 	 {Neuper, Walther},

   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},

   year = 	 {2016},

   address = {Bialystok, Poland},

   month = {July 25-29},

   pages = {83-89},

   note = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}}

 }

 @Misc{wn:lucin-thedu18,

   author = 	 {Walther Neuper},

   title = 	 {Lucas-Interpretation from Programmers' Perspective},

   year = 	 {2018},

   note = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}}

 }

 @InProceedings{wn:lucas-interp-12,

   author    = "Neuper, Walther",

   year      = "2012",

   title     = "Automated Generation of User Guidance by Combining Computation and Deduction",

   pages     = "82-101",

   doi       = "10.4204/EPTCS.79.5",

   booktitle = {Electronic Proceedings in Theoretical Computer Science},

   editor    = "Quaresma, Pedro and Back, Ralph-Johan",

   volume    = "79",

   publisher = "Open Publishing Association"

 }

 @Book{progr-mathematica-2012,

   author = 	 {Maeder, Roman E.},

   title = 	 {Programming in Mathematica},

   publisher = 	 {Addison-Wesley},

   address = 	 {Reading, Mass.},

   year = 	 {2012},

   edition = 	 {3rd}

 }

 @PhdThesis{wn:diss,

   author = 	 {Neuper, Walther },

   title = 	 {Reactive User-Guidance by an Autonomous Engine Doing High-School Math},

   school = 	 {IICM - Inst. f. Softwaretechnology},

   year = 	 {2001},

   address = 	 {Technical University, A-8010 Graz},

   note = 	{\url{http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz}}

 }

 @Article{plmms10,

   author = 	 {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},

   title = 	 {{CTP}-based programming languages~? {C}onsiderations about an experimental design},

   journal = 	 {ACM Communications in Computer Algebra},

   doi = {10.1145/1838599.1838621},

   year = 	 {2010},

   volume = 	 {44},

   number = 	 {1/2},

   pages = 	 {27-41},

   month = 	 {March/June}

 }

 @Article{back-SD-2010,

   author = 	 {R.-J. Back},

   title = 	 {Structured derivations: a unified proof style for teaching mathematics},

   journal = 	 {Formal Aspects of Computing},

   year = 	 {2010},

   volume = 	 {22},

   number = 	 {5},

   pages = 	 {629-661}

 }

 @MastersThesis{mlehnf:bakk-11,

   author = 	 {Mathias Lehnfeld},

   title = 	 {Verbindung von 'Computation' und 'Deduction' im \sisac-System},

   school = 	 {Institut f\"ur Computersprachen, Technische Universit\"at Wien},

   year = 	 {2011},

   note = 	 {Bakkalaureate project}

 }

 @incollection{paulson700,

   author        = {Lawrence C. Paulson},

   title         = {{Isabelle}: The Next 700 Theorem Provers},

   booktitle     = {Logic and Computer Science},

   editor        = {P. Odifreddi},

   pages         = {361-386},

   publisher     = {Academic Press},

   url           = {https://arxiv.org/abs/cs/9301106},

   year          = {1990}

 }

 @misc{RISC4777,

     author = {B. Buchberger},

     title = {{The Role of Mathematical Thinking for 21st Century Society}},

     language = {english},

     year = {2013},

     month = {March 4-6},

     annote = {2013-03-04-A},

     note = {Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education},

     institution = {Khemarak University, Phnom Penh, Cambodia},

     conferencename = {The 2nd International Conference on Mathematics and Technology in Mathematics Education}

 }

 @Article{EMS-math-ethics,

   author = {Chiodo, Maurice and Clifton, Toby},

   title = {The Importance of Ethics in Mathematics},

   journal = {Newsletter of the European Mathematical Society},

   year = {2019},

   volume = {114},

   pages = {34-37},

   month = {December},

   url = {\url{https://euro-math-soc.eu/newsletter}}

 }

 @MastersThesis{ggt02,

   author = 	 {Karnel, Stefan},

   title = 	 {Gr\"o{\ss}te gemeinsame Teiler in Polynomringen und Implementierung im \isac-Projekt},

   school = 	 {University of Technology, Institute of Mathematics},

   year = 	 {2002},

   address = 	 {Graz, Austria},

   month = 	 {Aug}

 }

 @InProceedings{gdaroczy-EP-13,

   author = 	 {Gabriella Dar\'{o}czy and Walther Neuper},

   title = 	 {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},

   booktitle = 	 {eJMT, the Electronic Journal of Mathematics \& Technology},

   year = 	 {2013},

   volume = 	 {7},

   pages = 	 {175-194},

   month = 	 {February},

   note = 	 {Special Issue ``TP-based Systems and Education''},

   url = {\url{https://php.radford.edu/~ejmt/ContentIndex.php\#v7n2}}

 }

 @TECHREPORT{tBaBoEr07a,

   author = {Back, Ralph-Johan and Bos, Victor and Eriksson, Johannes},

   title = {MathEdit: Tool Support for Structured Calculational Proofs},

   institution = {TUCS},

   year = {2007},

   number = {854},

   month = {Dec},

   note = {\url{http://tucs.fi/publications/view/?pub_id=tBaBoEr07a}}

 }

 @article{Farmer_al:93,

 author = {W. D. Farmer and J. D. Guttman and F. J. Thayer},

 title = {{IMPS: An Interactive Mathematical Proof System}},

 journal = {Journal of Automated Reasoning},

 year = {1993},

 volume = {11},

 month = {August},

 number = {2},

 pages = {213-248},

 }

 @InProceedings{gclc-06,

   author = 	 {Jani\v{c}i\'c, Predrag},

   title = 	 {{GCLC} --- a tool for constructive euclidean geometry and more than that},

   booktitle =    {Mathematical Software -- {ICMS} 2006},

   pages = 	 {58-73},

   year = 	 {2006},

   number = 	 {4151}

 }

 @Article{ggb:atp-15,

   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.},

   title = 	 {Automated Theorem Proving in {GeoGebra}: Current Achievements},

   journal = 	 {Journal of Automated Reasoning},

   year = 	 {2015},

   volume = 	 {55},

   number = 	 {1},

   pages = 	 {39-59},

   ISSN = 	 {0168-7433},

   DOI = 	 {http://dx.doi.org/10.1007/s10817-015-9326-4}

 }

 @Manual{isabelle-jedit,

   title = 	 {{Isabelle/jEdit}},

   author = 	 {Makarius Wenzel},

   address = 	 {Munich},

   note = 	 {Part of the Isabelle distribution},

   note = 	 {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}

 }

 @TechReport{Yacc-1975,

   author = {Johnson, Stephen C.},

   title = {Yacc: {Y}et {A}nother {C}ompiler-{C}ompiler},

   institution = {AT\&T Bell Laboratories},

   year = {1975},

   number = {32},

   address = {Murray Hill, New Jersey},

   note = {Retrieved 31 January 2020}

 }