Maths with Coq in L1, a pedagogical experiment
Maths with Coq in L1, a pedagogical experiment
In France, the first year of study at university is usually abbreviated L1 (for premiere annee de Licence). At Sorbonne Paris Nord University, we have been teaching an 18 hour introductory course in formal proofs to L1 students for 3 years. These students are in a double major mathematics and computer science curriculum. The course is mandatory and consists only of hands-on sessions with the Coq proof assistant. We present some of the practical sessions worksheets, the methodology we used to write them and some of the pitfalls we encountered. Finally we discuss how this course evolved over the years and will see that there is room for improvement in many different technical and pedagogical aspects.
Marie Kerjean、Micaela Mayero、Pierre Rousselin
CNRS, Université Sorbonne Paris Nord, Laboratoire d'informatique de Paris Nord, LIPN, Villetaneuse, FranceUniversité Sorbonne Paris Nord, Laboratoire d'informatique de Paris Nord, LIPN, Villetaneuse, France, Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, Gif-sur-Yvette, FranceUniversité Sorbonne Paris Nord, CNRS, Laboratoire Analyse, Géométrie et Applications, LAGA, Villetaneuse, France, Inria, Paris, CERMICS, école des ponts, Marne-la-Vallée, France
教育计算技术、计算机技术
Marie Kerjean,Micaela Mayero,Pierre Rousselin.Maths with Coq in L1, a pedagogical experiment[EB/OL].(2025-05-09)[2025-06-16].https://arxiv.org/abs/2505.05990.点此复制
评论