2 papers
cs.LO2025
A Rocq Formalization of Monomial and Graded Orders
Sylvie Boldo, François Clément, Vincent Martin +1
Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the fi…
cs.LO2025
Teaching Divisibility and Binomials with Coq
Sylvie Boldo, François Clément, David Hamelin +2
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 ta…