Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2505.05990 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909605969264640 |
|---|---|
| author | Kerjean, Marie Mayero, Micaela Rousselin, Pierre |
| author_facet | Kerjean, Marie Mayero, Micaela Rousselin, Pierre |
| contents | 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.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_05990 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Maths with Coq in L1, a pedagogical experiment Kerjean, Marie Mayero, Micaela Rousselin, Pierre Logic in Computer Science 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. |
| title | Maths with Coq in L1, a pedagogical experiment |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2505.05990 |