@inproceedings(EPTCS328.1,
 author       = {Ayala-Rinc\'on, Mauricio and Thaynara Arielly de Lima},
 year         = {2020},
 title        = {Teaching Interactive Proofs to Mathematicians},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 9th International Workshop on} Theorem Proving Components for Educational Software, {\rm Paris, France, 29th June 2020}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {328},
 publisher    = {Open Publishing Association},
 pages        = {1--17},
 doi          = {10.4204/EPTCS.328.1},
)
@book(Ralph-Johan06a,
 author       = {Ralph-Johan Back and Joakim von Wright},
 year         = {2006},
 title        = {Mathematics with a Little Bit of Logic: Structured Derivations in High-School Mathematics},
 publisher    = {Manuscript},
)
@inproceedings(kit-math-expr-OCR-2019,
 author       = {Sidney Bender and Monica Haurilet and Alina Roitberg and Rainer Stiefelhagen},
 year         = {2019},
 title        = {Learning Fine-Grained Image Representations for Mathematical Expression Recognition},
 booktitle    = {2019 International Conference on Document Analysis and Recognition Workshops (ICDARW)},
 volume       = {1},
 pages        = {56--61},
 doi          = {10.1109/ICDARW.2019.00015},
)
@inproceedings(DBLP:conf/fm/BjornerH14,
 author       = {Bj{\o}rner, Dines and Klaus Havelund},
 year         = {2014},
 title        = {40 Years of Formal Methods - Some Obstacles and Some Possibilities?},
 booktitle    = {{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings},
 pages        = {42--61},
 doi          = {10.1007/978-3-319-06410-9_4},
)
@inproceedings(EPTCS328.4,
 author       = {Merlin Carl},
 year         = {2020},
 title        = {Number Theory and Axiomatic Geometry in the Diproche System},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 9th International Workshop on} Theorem Proving Components for Educational Software, {\rm Paris, France, 29th June 2020}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {328},
 publisher    = {Open Publishing Association},
 pages        = {56--78},
 doi          = {10.4204/EPTCS.328.4},
)
@inproceedings(EPTCS313.3,
 author       = {David M. Cerna and Rafael P.D. Kiesel and Alexandra Dzhiganskaya},
 year         = {2020},
 title        = {A Mobile Application for Self-Guided Study of Formal Reasoning},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 8th International Workshop on} Theorem Proving Components for Educational Software, {\rm Natal, Brazil, 25th August 2019}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {313},
 publisher    = {Open Publishing Association},
 pages        = {35--53},
 doi          = {10.4204/EPTCS.313.3},
)
@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''},
)
@inproceedings(farmer:eduIMPS,
 author       = {William M. Farmer},
 year         = {2000},
 title        = {A proposal for the development of an interactive mathematics laboratory for mathematics eduction},
 booktitle    = {CADE-17 Workshop on Deduction Systems for Mathematics Education},
 pages        = {20--25},
)
@inproceedings(EPTCS328.2,
 author       = {Asta Halkj{\ae}r From and J{\o}rgen Villadsen and Patrick Blackburn},
 year         = {2020},
 title        = {Isabelle/{HOL} as a Meta-Language for Teaching Logic},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 9th International Workshop on} Theorem Proving Components for Educational Software, {\rm Paris, France, 29th June 2020}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {328},
 publisher    = {Open Publishing Association},
 pages        = {18--34},
 doi          = {10.4204/EPTCS.328.2},
)
@book(gries,
 author       = {David Gries},
 year         = {1981},
 title        = {The science of programming},
 series       = {Texts and monographs in computer science},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-1-4612-5983-1},
)
@book(ICMI19-2012,
 editor       = {Gila Hanna and Michael de Villiers},
 year         = {2012},
 title        = {Proof and Proving in Mathematics Education. The 19th ICMI Study},
 series       = {New ICMI Study Series},
 volume       = {15},
 publisher    = {Springer},
)
@inproceedings(logic-tutors-11,
 author       = {Antonia Huertas},
 year         = {2011},
 title        = {Ten Years of Computer-based Tutors for Teaching Logic 2000-2010: Lessons Learned},
 booktitle    = {Proceedings of the Third International Congress Conference on Tools for Teaching Logic (TICTTL’11)},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {131--140},
 doi          = {10.1093/jigpal/jzm019},
)
@inproceedings(prajaks1,
 author       = {P. Jitngernmadan and K. Miesenberger},
 year         = {2015},
 title        = {A Comparative Study on Java Technologies for Focus and Cursor Handling in Accessible Dynamic Interactions},
 editor       = {Sikne Lanyi, C.},
 booktitle    = {Proceedings of {AAATE}},
 publisher    = {IOS Press, Amsterdam},
 address      = {Budapest},
)
@inproceedings(prajaks4,
 author       = {P. Jitngernmadan and K. Miesenberger},
 year         = {2017},
 title        = {Extraction Methodology of Implicit Didactics in Math Schoolbooks for the Blind},
 editor       = {P. Cudd and De Witte, L.},
 booktitle    = {Proceedings AAATE Conference 2017. Harnessing the Power of Technology to Improve Lives},
 publisher    = {IOS Press},
 address      = {Amsterdam},
)
@inproceedings(prajaks2,
 author       = {P. Jitngernmadan and A. Petz and B. St\"oger and K. Miesenberger},
 year         = {2016},
 title        = {Analysis of Implicit Didactics in Math Schoolbooks for Interactive Non-visual User Interface Development},
 editor       = {K. Miesenberger and C. Bühler and P. Penaz},
 booktitle    = {Computers Helping People with Special Needs, 15th International Conference, {ICCHP} 2016},
 publisher    = {Springer Heidelberg},
 address      = {Linz Austria},
 doi          = {10.1007/978-3-319-41264-1_3},
)
@article(prajaks3,
 author       = {P. Jitngernmadan and B. St\"oger and A Petz and K. Miesenberger},
 year         = {2017},
 title        = {{IDMILE}: An interactive didactic math inclusion learning environment for blind students},
 journal      = {Technology and Disability},
 volume       = {29},
 number       = {1-2},
 pages        = {47--61},
 doi          = {10.3233/TAD-170173},
)
@phdthesis(prajaks:phd,
 author       = {Prajaks Jitngernmadan},
 year         = {2017},
 title        = {A Framework of Support Functionalities for Multimodal Interface Design for Mathematic Working Environment},
 school       = {Johannes Kepler University Linz},
 address      = {Austria},
)
@mastersthesis(nkarl:master,
 author       = {Natalie Karl},
 year         = {2016},
 title        = {Developing an Inclusive Approach for Representing Mathematical Formulas},
 school       = {Hagenberg University of Applied Sciences},
 address      = {Linz, Austria},
 note         = {\url{https://static.miraheze.org/isacwiki/0/02/Masterthesis_NatalieKarl.pdf}},
)
@article(EMS-STT-19,
 author       = {Boris Koichu and Alon Pinto},
 year         = {2019},
 title        = {The Secondary-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},
)
@article(stellungn-dmv-gdm-mnu,
 author       = {W. Kopef and M R\"ockner and A. Eichler and G. Heckmann},
 year         = {2017},
 title        = {Zur aktuellen {D}iskussion \"uber die {Q}ualit\"at des {M}athematikunterrichts},
 journal      = {Mitteilungen der Deutschen Mathematiker-Vereinigung},
 volume       = {25},
 number       = {1},
 pages        = {6--7},
 doi          = {10.1515/dmvm-2017-0005},
)
@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},
)
@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(pl:lucas70,
 author       = {Peter Lucas and Kurt Walk},
 year         = {1970},
 title        = {On the Formal Description of PL/I},
 series       = {Annual Review in Automatic Programming},
 volume       = {6},
 publisher    = {Pergamon Press},
 address      = {Oxford},
)
@mastersthesis(mahringer,
 author       = {Marco Mahringer},
 year         = {2018},
 title        = {Formula Editors for {TP}-based Systems. State of the Art and Prototype Implementation in \textit{ISAC}},
 school       = {University of Applied Sciences},
 address      = {Hagenberg, Austria},
 note         = {\url{https://static.miraheze.org/isacwiki/d/d7/Mmahringer-master.pdf}},
)
@inproceedings(ActiveMath-MAIN11,
 author       = {Erica Melis and J\"org Siekmann},
 year         = {2004},
 title        = {An Intelligent Tutoring System for Mathematics},
 editor       = {L. Rutkowski and J. Siekmann and R. Tadeusiewicz and L.A. Zadeh},
 booktitle    = {Seventh International Conference ’Artificial Intelligence and Soft Computing’ (ICAISC)},
 series       = {LNAI},
 volume       = {3070,},
 publisher    = {Springer-Verlag},
 pages        = {91–101},
 doi          = {10.1007/978-3-540-24844-6\_12},
)
@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(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},
)
@inproceedings(EPTCS-wn-20,
 author       = {Walther Neuper},
 year         = {2020},
 title        = {Lucas-{I}nterpretation on {I}sabelle's {F}unctions},
 editor       = {Pedro Quaresma and Walther Neuper and Jo\~ao Marcos},
 booktitle    = {{\rm Proceedings 9th International Workshop on} Theorem Proving Components for Educational Software, {\rm Paris, France, 29th June 2020}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {328},
 publisher    = {Open Publishing Association},
 pages        = {79--95},
 doi          = {10.4204/EPTCS.328.5},
)
@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},
)
@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},
)
@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},
)
@book(Nipkow-Paulson-Wenzel:2002,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2002},
 title        = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
 series       = {LNCS},
 volume       = {2283},
 publisher    = {Springer},
 doi          = {10.1007/3-540-45949-9},
)
@incollection(PISA-math-2015,
 author       = {{OECD}},
 year         = {2017},
 title        = {{PISA} 2015 Mathematics Framework},
 booktitle    = {PISA 2015 Assessment and Analytical Framework: Science, Reading, Mathematic, Financial Literacy and Collaborative Problem Solving},
 publisher    = {OECD Publishing},
 address      = {Paris},
 doi          = {10.1787/9789264281820-5-en},
)
@inproceedings(blanchette:sledgehammer,
 author       = {Lawrence C. Paulson and Jasmin C. Blanchette},
 year         = {2010},
 title        = {Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers},
 editor       = {Schulz S. Sutcliffe G., Ternovska E.},
 booktitle    = {IWIL 2010},
 publisher    = {Springer},
 note         = {\url{http://people.mpi-inf.mpg.de/~jblanche/iwil2010-sledgehammer.pdf}},
)
@article(LCF-to-Isabelle-HOL:2019,
 author       = {Lawrence C. Paulson and Tobias Nipkow and Makarius Wenzel},
 year         = {2019},
 title        = {From {LCF} to {Isabelle/HOL}},
 journal      = {Formal Aspects of Computing},
 volume       = {31},
 pages        = {675--698},
 doi          = {10.1007/s00165-019-00492-1},
 note         = {Springer, London},
)
@inproceedings(RISC5531,
 author       = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},
 year         = {2018},
 title        = {{Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models}},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{Post-Proceedings ThEdu'17}},
 series       = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
 volume       = {267},
 publisher    = {Open Publishing Association},
 pages        = {120--139},
 doi          = {10.4204/EPTCS.267.8},
)
@inproceedings(inftyreader,
 author       = {M. Suzuki and F. Tamari and R. Fukuda and S. Uchida and T. Kanahori},
 year         = {2003},
 title        = {Infty ? an integrated OCR system for mathematical documents},
 booktitle    = {Proc. {ACA} Symposium on Document Engineering},
 pages        = {95--104},
)
@inproceedings(chattyinfty2,
 author       = {M. Suzuki and K. Yamaguchi},
 year         = {2020},
 title        = {On Automatic Conversion from e-Born PDF into Accessible EPUB3 and Audio-Embedded HTML5},
 booktitle    = {Proc. the 17th International Conference on Computers Helping People with Special Needs ({ICCHP} 2020)},
 series       = {LNCS},
 volume       = {12376},
 publisher    = {Springer},
 pages        = {410--416},
 doi          = {10.1007/978-3-030-58796-3_48},
)
@incollection(Wenzel:2006:Festschrift,
 author       = {Makarius Wenzel},
 year         = {2007},
 title        = {{Isabelle/Isar} --- a generic framework for human-readable proof documents},
 editor       = {R. Matuszewski and A. Zalewska},
 booktitle    = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
 series       = {Studies in Logic, Grammar, and Rhetoric},
 volume       = {10(23)},
 publisher    = {University of Bia{\l}ystok},
 url          = {https://www21.in.tum.de/~wenzelm/papers/isar-framework.pdf},
)
@inproceedings(Wenzel:2019:MKM,
 author       = {Makarius Wenzel},
 year         = {2019},
 title        = {Interaction with Formal Mathematical Documents in {Isabelle/PIDE}},
 editor       = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Sacerdoti Coen, Claudio},
 booktitle    = {Intelligent Computer Mathematics (CICM 2019)},
 volume       = {11617},
 publisher    = {Springer},
 doi          = {10.48550/arXiv.1905.01735},
)
@manual(isa-system-2021,
 author       = {Makarius Wenzel},
 year         = {2021},
 title        = {The Isabelle System Manual},
 url          = {https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf},
 note         = {Contained in the Isabelle distribution},
)
@misc(IsaWS-22,
 author       = {W.Neuper and B.St\"oger and M.Wenzel},
 year         = {2022},
 title        = {Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode},
 howpublished = {Isabelle Workshop 2022 \url{https://sketis.net/isabelle/isabelle-workshop-2022}},
 note         = {Accessed: 202-10-13},
)
@article(chattyinfty1,
 author       = {K. Yamaguchi and M. Suzuki},
 year         = {2019},
 title        = {An accessible {STEM} editor customizable for various local languages},
 journal      = {Journal of Enabling Technologies},
 volume       = {13},
 number       = {4},
 pages        = {240--250},
 doi          = {10.1108/JET-12-2018-0064},
)