Saved in:
Bibliographic Details
Main Authors: Boldo, Sylvie, Clément, François, Hamelin, David, Mayero, Micaela, Rousselin, Pierre
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2404.12676
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866913849115934720
author Boldo, Sylvie
Clément, François
Hamelin, David
Mayero, Micaela
Rousselin, Pierre
author_facet Boldo, Sylvie
Clément, François
Hamelin, David
Mayero, Micaela
Rousselin, Pierre
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2404_12676
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Teaching Divisibility and Binomials with Coq
Boldo, Sylvie
Clément, François
Hamelin, David
Mayero, Micaela
Rousselin, Pierre
Logic in Computer Science
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.
title Teaching Divisibility and Binomials with Coq
topic Logic in Computer Science
url https://arxiv.org/abs/2404.12676