Archive of Formal Proofs.
http://afp.sourceforge.net.
S. Amani, A. Hixon, Z. Chen, C. Rizkallah, P. Chubb, L. O’Connor, J. Beeren, Y. Nagashima, J. Lim, T. Sewell, J. Tuong, G. Keller, T. Murray, G. Klein & G. Heiser (2016):
Cogent: Verifying High-Assurance File System Implementations.
In: International Conference on Architectural Support for Programming Languages and Operating Systems.
Springer Berlin / Heidelberg,
Atlanta, GA, USA,
pp. 175–188,
doi:10.1145/2872362.2872404.
R.-J. Back (2010):
Structured derivations: a unified proof style for teaching mathematics.
Formal Aspects of Computing 22(5),
pp. 629–661,
doi:10.1007/s00165-009-0136-5.
Ralph-Johan Back, Victor Bos & Johannes Eriksson (2007):
MathEdit: Tool Support for Structured Calculational Proofs.
Technical Report 854.
TUCS.
Available at http://tucs.fi/publications/view/?pub_id=tBaBoEr07a.
F. Botana, M. Hohenwarter, P. Janiči\'c, Z. Kovács, I. Petrovi\'c, T. Recio & S. Weitzhofer (2015):
Automated Theorem Proving in GeoGebra: Current Achievements.
Journal of Automated Reasoning 55(1),
pp. 39–59,
doi:10.1007/s10817-015-9326-4.
B. Buchberger (2013):
The Role of Mathematical Thinking for 21st Century Society.
Invited talk at The 2nd International Conference on Mathematics and Technology in Mathematics Education.
Jasmin C.Blanchette:
Hammering Away. A User's Guide to Sledgehammer for Isabelle/HOL.
contained in the Isabelle distribution.
Available at http://isabelle.in.tum.de/doc/sledgehammer.pdf.
David M. Cerna (2019):
Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire.
RISC Report Series.
Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz,
Schloss Hagenberg, 4232 Hagenberg, Austria.
Maurice Chiodo & Toby Clifton (2019):
The Importance of Ethics in Mathematics.
Newsletter of the European Mathematical Society 114,
pp. 34–37,
doi:10.4171/NEWS/114/9.
Gabriella Daróczy & Walther Neuper (2013):
Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems.
In: eJMT, the Electronic Journal of Mathematics & Technology 7,
pp. 175–194.
Available at https://php.radford.edu/~ejmt/ContentIndex.php#v7n2.
Special Issue ``TP-based Systems and Education''.
W. D. Farmer, J. D. Guttman & F. J. Thayer (1993):
IMPS: An Interactive Mathematical Proof System.
Journal of Automated Reasoning 11(2),
pp. 213–248,
doi:10.1007/BF00881906.
Florian Haftmann, Cezary Kaliszyk & Walther Neuper (2010):
CTP-based programming languages ? Considerations about an experimental design.
ACM Communications in Computer Algebra 44(1/2),
pp. 27–41,
doi:10.1145/1838599.1838621.
Florian Haftmann & Tobias Nipkow (2010):
Code Generation via Higher-Order Rewrite Systems.
In: Matthias Blume, Naoki Kobayashi & Germán Vidal: Functional and Logic Programming,
Lecture Notes in Computer Science 6009.
Springer Berlin / Heidelberg,
pp. 103–117,
doi:10.1007/978-3-642-12251-4_9.
Predrag Janiči\'c (2006):
GCLC — a tool for constructive euclidean geometry and more than that.
In: Mathematical Software – ICMS 2006 4151,
pp. 58–73,
doi:10.1007/11812289_22.
Stephen C. Johnson (1975):
Yacc: Yet Another Compiler-Compiler.
Technical Report 32.
AT&T Bell Laboratories,
Murray Hill, New Jersey.
Retrieved 31 January 2020.
Boris Koichu & Alon Pinto (2019):
The Seoncdary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?.
EMS Newsletter,
pp. 34–35,
doi:10.4171/NEWS.
Alexander Krauss (2006):
Partial Recursive Functions in Higher-Order Logic.
In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, Third International Joint Conference, IJCAR 2006,
Lecture Notes in Computer Science 4130.
Springer,
pp. 589–603,
doi:10.1007/11814771_48.
Alan Krempler & Walther Neuper (2018):
Prototyping ``Systems that Explain Themselves'' for Education.
In: Pedro Quaresma & Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017,
Electronic Proceedings in Theoretical Computer Science 267.
Open Publishing Association,
pp. 89–107,
doi:10.4204/EPTCS.267.6.
Mathias Lehnfeld (2011):
Verbindung von 'Computation' und 'Deduction' im ISAC-System.
Institut für Computersprachen, Technische Universität Wien.
Bakkalaureate project.
Peter Lucas (1978):
On the Formalization of Programming Languages: Early History and Main Approaches.
In: D. Bjørner & C. B. Jones: The Vienna Development Method: The Meta-Language,
LNCS 16.
Springer,
doi:10.1007/3-540-08766-4_8.
Roman E. Maeder (2012):
Programming in Mathematica,
3rd edition.
Addison-Wesley,
Reading, Mass..
Walther Neuper (2001):
Reactive User-Guidance by an Autonomous Engine Doing High-School Math.
IICM - Inst. f. Softwaretechnology,
Technical University, A-8010 Graz.
Available at https://static.miraheze.org/isacwiki/8/8a/Wn-diss.pdf.
Walther Neuper (2012):
Automated Generation of User Guidance by Combining Computation and Deduction.
In: Pedro Quaresma & Ralph-Johan Back: Electronic Proceedings in Theoretical Computer Science 79.
Open Publishing Association,
pp. 82–101,
doi:10.4204/EPTCS.79.5.
Walther Neuper (2014):
GCD — A Case Study on Lucas-Interpretation.
In: Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM,
Coimbra, Portugal.
Available at http://ceur-ws.org/Vol-1186/paper-17.pdf.
Urn:nbn:de:0074-1186-1.
Walther Neuper (2016):
Lucas-Interpretation from Users' Perspective.
In: Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics,
Bialystok, Poland,
pp. 83–89.
Available at http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf.
Urn:nbn:de:0074-1785-8.
Walther Neuper (2018):
Mechanical Explanation in ``Systems that explain themselves''.
In: Osman Hasan: Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018.
Conference on Intelligent Computer Mathematics CICM,
Hagenberg, Austria.
Available at https://www.cicm-conference.org/2018/infproc/paper1.pdf.
Urn:nbn:de:0074-2307-7.
Walther Neuper (2019):
Technologies for "Complete, Transparent & Interactive Models of Math" in Education.
In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 july 2018,
Electronic Proceedings in Theoretical Computer Science 290.
Open Publishing Association,
pp. 76–95,
doi:10.4204/EPTCS.290.6.
Walther Neuper & Christian Dürnsteiner (2007):
Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software.
Technical Report 683.
IMST – Innovationen Machen Schulen Top!,
University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.
Available at https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf.
Walther Neuper, Johannes Reitinger & Angelika Gründlinger (2008):
Begreifen und Mechanisieren beim Algebra Einstieg.
Technical Report 1063.
IMST – Innovationen Machen Schulen Top!,
University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.
Available at https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf.
Walther Neuper (2006):
Angewandte Mathematik und Fachtheorie.
Technical Report 357.
IMST – Innovationen Machen Schulen Top!,
University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.
Available at http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie.
Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2008):
Isabelle/HOL, a proof assistant for high-order logic.
Springer Verlag.
Lawrence C. Paulson (1990):
Isabelle: The Next 700 Theorem Provers.
In: P. Odifreddi: Logic and Computer Science.
Academic Press,
pp. 361–386.
Available at https://arxiv.org/abs/cs/9301106.
Pedro Quaresma & Ralph-Johan Back (2012):
Proceedings First Workshop on CTP Components for Educational Software (THedu'11) 79.
Open Publishing Association,
doi:10.4204/EPTCS.79.
Y. Shi, Y. Ma & J. MacLeod (2019):
College students’ cognitive learning outcomes in flipped classroom instruction: a meta-analysis of the empirical literature.
Journal of Computers in Education,
pp. 1–25,
doi:10.1007/s40692-019-00142-8.
Makarius Wenzel (2014):
System description: Isabelle/jEdit in 2014.
In: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014.,
pp. 84–94,
doi:10.4204/EPTCS.167.10.
eptcs@eptcs.org