Coq/Rocq tutorial: Ssreflect tactics and the MathComp library | Vidéo | Carmin.tv

00:00:00 / 00:00:00

Coq/Rocq tutorial: Ssreflect tactics and the MathComp library

By Marie Kerjean

Appears in collection : Lean for the curious mathematician / Lean pour mathématiciens

In this talk, we introduce the Ssreflect tactic language, as used in the Mathematical Components library. We will focus on the tactics used to make formalization work lighter and easier to maintain.

Information about the video

Date of recording 28/03/2024
Date of publication 22/04/2024
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Guillaume Hennenfent
Format MP4

Citation data

DOI 10.24350/CIRM.V.20153503
Cite this video Kerjean, Marie (28/03/2024). Coq/Rocq tutorial: Ssreflect tactics and the MathComp library. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.20153503
URL https://dx.doi.org/10.24350/CIRM.V.20153503

Domain(s)

Logic in Computer Science

MSC codes

03B35 Mechanization of proofs and logical operations

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow

Copyright Carmin.tv 2026

Give feedback