Teaching Divisibility and Binomials with Coq
The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials.These basic topics are a good case study as they are widely taught in the early academic years (or before in France).We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students.As expected, it required additional Coq material such as other lemmas and dedicated tactics.The worksheets are freely available and flexible in several ways.
Authors
- Sylvie Boldo (ORCID: https://orcid.org/0000-0002-1970-3019)
- Pierre Rousselin
- Micaela Mayero
- David Hamelin
- François Clément (ORCID: https://orcid.org/0000-0001-9206-3698)
Institutions
- Université Paris-Saclay (FR)
- Université Sorbonne Paris Nord (FR)
- Laboratoire Analyse, Géométrie et Applications (FR)
- CERMICS (FR)
- Laboratoire d'Informatique de Paris-Nord (FR)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2025-05-07
- DOI
- https://doi.org/10.4204/eptcs.419.8
- Citations
- 1
- Primary Topic
- History and Theory of Mathematics
- Type
- article
- Field-Weighted Citation Impact
- 28.58
Funders
- European Commission