Français
Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
Multi angle
Authors : Kerjean, Marie (Author of the conference)
CIRM (Publisher )
03B35 - Mechanization of proofs and logical operations
CIRM (Publisher )
Loading the player...
|
Abstract :
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
MSC Codes : Keywords : Proof assistant; Coq proof assistant; libraries of formalized mathematics; Mathematical Components; Ssreflect tactic language
03B35 - Mechanization of proofs and logical operations
|
Information on the Video
Film maker : Hennenfent, GuillaumeLanguage : English Available date : 22/04/2024 Conference Date : 28/03/2024 Subseries : Research talks arXiv category : Logic in Computer Science Mathematical Area(s) : Logic and Foundations Format : MP4 (.mp4) - HD Video Time : 01:34:11 Targeted Audience : Researchers ; Graduate Students ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2024-03-28_Kerjean.mp4 
|
Information on the Event
Event Title : Lean for the curious mathematician / Lean pour mathématiciensEvent Organizers : Brasca, Riccardo ; Chambert-Loir, Antoine ; de Frutos-Fernández, María Inés ; Nuccio , Filippo Dates : 25/03/2024 - 29/03/2024 Event Year : 2024 Event URL : https://conferences.cirm-math.fr/2970.html
Citation Data
DOI : 10.24350/CIRM.V.20153503Cite this video as: 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 |
See Also
- [Multi angle] Stone duality and its formalization / Author of the conference van Gool, Sam.
- [Multi angle] Working with Mathlib / Author of the conference Loreaux, Jireh.
- [Multi angle] Complex analysis in Lean / Author of the conference Beffara, Vincent.
Bibliography
Imagette Video
