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

De Marie Kerjean

Apparaît dans la 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.

Informations sur la vidéo

Date de captation 28/03/2024
Date de publication 22/04/2024
Institut CIRM
Licence CC BY NC ND
Langue Anglais
Audience Chercheurs, Doctorants
Réalisateur(s) Guillaume Hennenfent
Format MP4

Données de citation

DOI 10.24350/CIRM.V.20153503
Citer cette vidéo 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

Domaine(s)

Logique en informatique

Codes MSC

03B35 Mechanization of proofs and logical operations

Dernières questions liées sur MathOverflow

Pour poser une question, votre compte Carmin.tv doit être connecté à mathoverflow

Poser une question sur MathOverflow

Copyright Carmin.tv 2026

Donner son avis