En poursuivant votre navigation sur ce site, vous acceptez l'utilisation d'un simple cookie d'identification. Aucune autre exploitation n'est faite de ce cookie. OK
1

Coq/Rocq tutorial: Ssreflect tactics and the MathComp library

Sélection Signaler une erreur
Multi angle
Auteurs : Kerjean, Marie (Auteur de la conférence)
CIRM (Editeur )

Loading the player...

Résumé : 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.

Mots-Clés : Proof assistant; Coq proof assistant; libraries of formalized mathematics; Mathematical Components; Ssreflect tactic language

Codes MSC :
03B35 - Mechanization of proofs and logical operations

    Informations sur la Vidéo

    Réalisateur : Hennenfent, Guillaume
    Langue : Anglais
    Date de Publication : 22/04/2024
    Date de Captation : 28/03/2024
    Sous Collection : Research talks
    Catégorie arXiv : Logic in Computer Science
    Domaine(s) : Logique et Fondements
    Format : MP4 (.mp4) - HD
    Durée : 01:34:11
    Audience : Chercheurs ; Etudiants Science Cycle 2 ; Doctoral Students, Post-Doctoral Students
    Download : https://videos.cirm-math.fr/2024-03-28_Kerjean.mp4

Informations sur la Rencontre

Nom de la Rencontre : Lean for the curious mathematician / Lean pour mathématiciens
Organisateurs de la Rencontre : Brasca, Riccardo ; Chambert-Loir, Antoine ; de Frutos-Fernández, María Inés ; Nuccio , Filippo
Dates : 25/03/2024 - 29/03/2024
Année de la rencontre : 2024
URL de la Rencontre : https://conferences.cirm-math.fr/2970.html

Données de citation

DOI : 10.24350/CIRM.V.20153503
Citer cette vidéo: Kerjean, Marie (2024). Coq/Rocq tutorial: Ssreflect tactics and the MathComp library. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.20153503
URI : http://dx.doi.org/10.24350/CIRM.V.20153503

Voir Aussi

Bibliographie



Imagette Video

Sélection Signaler une erreur