English
Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
Multi angle
Auteurs : Kerjean, Marie (Auteur de la Conférence)
CIRM (Editeur )
03B35 - Mechanization of proofs and logical operations
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.
Keywords : Proof assistant; Coq proof assistant; libraries of formalized mathematics; Mathematical Components; Ssreflect tactic language
Codes MSC : Keywords : Proof assistant; Coq proof assistant; libraries of formalized mathematics; Mathematical Components; Ssreflect tactic language
03B35 - Mechanization of proofs and logical operations
|
Informations sur la Vidéo
Réalisateur : Hennenfent, GuillaumeLangue : Anglais Date de publication : 22/04/2024 Date de captation : 28/03/2024 Sous collection : Research talks arXiv category : Logic in Computer Science Domaine : Logic and Foundations Format : MP4 (.mp4) - HD Durée : 01:34:11 Audience : Researchers ; Graduate Students ; 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ématiciensOrganisateurs 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 Congrès : https://conferences.cirm-math.fr/2970.html
Données de citation
DOI : 10.24350/CIRM.V.20153503Citer 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
- [Multi angle] Stone duality and its formalization / Auteur de la Conférence van Gool, Sam.
- [Multi angle] Working with Mathlib / Auteur de la Conférence Loreaux, Jireh.
- [Multi angle] Complex analysis in Lean / Auteur de la Conférence Beffara, Vincent.
Bibliographie
Imagette Video
