1. INRIA - The Coq webpage.
  2. 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.
  3. 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.
  4. Nathan C Carter & Kenneth G Monks: Using the Proof-Checking Word Processor Lurch to Teach Proof-Writing. Available at .
  5. Allan Collins, John Seely Brown & Ann Holum (1991): Cognitive apprenticeship: Making thinking visible. American educator 15(3), pp. 6–11.
  6. 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.
  7. H James Hoover & Piotr Rudnicki (1996): Teaching freshman logic with MIZAR-MSE. In: Workshop on Teaching Logic and Reasoning in an Illogical World.
  8. 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.
  9. 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.
  10. 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.
  11. Julien Narboux: Toward the use of a proof assistant to teach mathematics..
  12. 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.
  13. Krzysztof Retel & Anna Zalewska (2005): Mizar as a Tool for Teaching Mathematics. Mechanized Mathematics and Its Applications 4(1), pp. 35–42.
  14. Jakub Sakowicz & Jacek Chrząszcz (2007): Papuq: a Coq assistant. Proceedings of PATE 7, pp. 79–96.
  15. Andrzej Trybulec & Peter Rudnicki (1993): Using Mizar in Computer Aided Instruction of Mathematics. In: Norvegian-French Conference of CAI in Mathematics.
  16. Makarius Wenzel (2017): The Isabelle/Isar Reference Manual. Available at .

Comments and questions to:
For website issues: