@(inria,
title = {{INRIA - The Coq webpage}},
)
@article(back2010,
author = {Ralph{-}Johan Back},
year = {2010},
title = {{Structured derivations: a unified proof style for teaching mathematics}},
journal = {Formal Aspects of Computing},
volume = {22},
number = {5},
pages = {629--661},
doi = {10.1007/s00165-009-0136-5},
)
@book(bertot2004,
author = {Yves Bertot and Pierre Cast{\'{e}}ran},
year = {2004},
title = {{Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions}},
series = {Texts in Theoretical Computer Science. An {EATCS} Series},
publisher = {Springer},
doi = {10.1007/978-3-662-07964-5},
)
@(carter2013,
author = {Nathan C Carter and Kenneth G Monks},
title = {{Using the Proof-Checking Word Processor Lurch to Teach Proof-Writing}},
url = {\url},
)
@article(collins1991,
author = {Allan Collins and John Seely Brown and Ann Holum},
year = {1991},
title = {{Cognitive apprenticeship: Making thinking visible}},
journal = {American educator},
volume = {15},
number = {3},
pages = {6--11},
)
@article(hendriks2010,
author = {Maxim Hendriks and Cezary Kaliszyk and Van Raamsdonk, Femke and Freek Wiedijk},
year = {2010},
title = {{Teaching logic using a state-of-the-art proof assistant}},
journal = {Acta Didactica Napocensia},
volume = {3},
number = {2},
pages = {35--48},
)
@inproceedings(hoover1996,
author = {H James Hoover and Piotr Rudnicki},
year = {1996},
title = {{Teaching freshman logic with MIZAR-MSE}},
booktitle = {{Workshop on Teaching Logic and Reasoning in an Illogical World}},
)
@inproceedings(knobelsdorf2016,
author = {Maria Knobelsdorf and Christiane Frede},
year = {2016},
title = {{Analyzing Student Practices in Theory of Computation in Light of Distributed Cognition Theory}},
booktitle = {Proceedings of the 2016 {ACM} Conference on International Computing Education Research, {ICER} 2016},
pages = {73--81},
doi = {10.1145/2960310.2960331},
)
@inproceedings(knobelsdorf2017,
author = {Maria Knobelsdorf and Christiane Frede and Sebastian B{\"{o}}hne and Christoph Kreitz},
year = {2017},
title = {{Theorem Provers as a Learning Tool in Theory of Computation}},
booktitle = {Proceedings of the 2017 {ACM} Conference on International Computing Education Research, {ICER} 2017},
pages = {83--92},
doi = {10.1145/3105726.3106184},
)
@inproceedings(knobelsdorf2014,
author = {Maria Knobelsdorf and Christoph Kreitz and Sebastian B{\"{o}}hne},
year = {2014},
title = {{Teaching Theoretical Computer Science using a Cognitive Apprenticeship Approach}},
booktitle = {The 45th {ACM} Technical Symposium on Computer Science Education, {SIGCSE} '14},
pages = {67--72},
doi = {10.1145/2538862.2538944},
)
@inproceedings(narboux2005,
author = {Julien Narboux},
title = {{Toward the use of a proof assistant to teach mathematics.}},
)
@inproceedings(nipkow2012,
author = {Tobias Nipkow},
year = {2012},
title = {{Teaching Semantics with a Proof Assistant: No More {LSD} Trip Proofs}},
booktitle = {{Verification, Model Checking, and Abstract Interpretation - 13th International Conference, {VMCAI} 2012}},
pages = {24--38},
doi = {10.1007/978-3-642-27940-9_3},
)
@article(retel2005,
author = {Krzysztof Retel and Anna Zalewska},
year = {2005},
title = {{Mizar as a Tool for Teaching Mathematics}},
journal = {Mechanized Mathematics and Its Applications},
volume = {4},
number = {1},
pages = {35--42},
)
@article(sakowicz2007,
author = {Jakub Sakowicz and Chrz{\k{a}}szcz, Jacek},
year = {2007},
title = {{Papuq: a Coq assistant}},
journal = {Proceedings of PATE},
volume = {7},
pages = {79--96},
)
@inproceedings(trybulec1993,
author = {Andrzej Trybulec and Peter Rudnicki},
year = {1993},
title = {{Using Mizar in Computer Aided Instruction of Mathematics}},
booktitle = {{Norvegian-French Conference of CAI in Mathematics}},
)
@misc(wenzel2017,
author = {Makarius Wenzel},
year = {2017},
title = {{The Isabelle/Isar Reference Manual}},
url = {\url},
)