Ralph-Johan 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.
Yves Bertot & Pierre Castéran (2004):
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. An EATCS Series.
Springer,
doi:10.1007/978-3-662-07964-5.
Nathan C Carter & Kenneth G Monks:
Using the Proof-Checking Word Processor Lurch to Teach Proof-Writing.
Available at .
Allan Collins, John Seely Brown & Ann Holum (1991):
Cognitive apprenticeship: Making thinking visible.
American educator 15(3),
pp. 6–11.
Maxim Hendriks, Cezary Kaliszyk, Femke Van Raamsdonk & Freek Wiedijk (2010):
Teaching logic using a state-of-the-art proof assistant.
Acta Didactica Napocensia 3(2),
pp. 35–48.
H James Hoover & Piotr Rudnicki (1996):
Teaching freshman logic with MIZAR-MSE.
In: Workshop on Teaching Logic and Reasoning in an Illogical World.
Maria Knobelsdorf & Christiane Frede (2016):
Analyzing Student Practices in Theory of Computation in Light of Distributed Cognition Theory.
In: Proceedings of the 2016 ACM Conference on International Computing Education Research, ICER 2016,
pp. 73–81,
doi:10.1145/2960310.2960331.
Maria Knobelsdorf, Christiane Frede, Sebastian Böhne & Christoph Kreitz (2017):
Theorem Provers as a Learning Tool in Theory of Computation.
In: Proceedings of the 2017 ACM Conference on International Computing Education Research, ICER 2017,
pp. 83–92,
doi:10.1145/3105726.3106184.
Maria Knobelsdorf, Christoph Kreitz & Sebastian Böhne (2014):
Teaching Theoretical Computer Science using a Cognitive Apprenticeship Approach.
In: The 45th ACM Technical Symposium on Computer Science Education, SIGCSE '14,
pp. 67–72,
doi:10.1145/2538862.2538944.
Julien Narboux:
Toward the use of a proof assistant to teach mathematics..
Tobias Nipkow (2012):
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs.
In: Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012,
pp. 24–38,
doi:10.1007/978-3-642-27940-9_3.
Krzysztof Retel & Anna Zalewska (2005):
Mizar as a Tool for Teaching Mathematics.
Mechanized Mathematics and Its Applications 4(1),
pp. 35–42.
Jakub Sakowicz & Jacek Chrząszcz (2007):
Papuq: a Coq assistant.
Proceedings of PATE 7,
pp. 79–96.
Andrzej Trybulec & Peter Rudnicki (1993):
Using Mizar in Computer Aided Instruction of Mathematics.
In: Norvegian-French Conference of CAI in Mathematics.
Makarius Wenzel (2017):
The Isabelle/Isar Reference Manual.
Available at .
eptcs@eptcs.org