add Marie and Cyril's lecture (#119)

Author: affeldt-aist

documentation.html

@@ -10,24 +10,36 @@
 #+HTML_HEAD: <style type="text/css"> h3 {margin-left: 1em; padding: 0px; color: #C05001;} </style>
 #+HTML_HEAD: <style type="text/css"> body { max-width: 1100px; width: 100% - 30px; margin-left: 30px; }</style>
 
-* Books
+* @@html:&#128218;@@ Books
 - [[https://math-comp.github.io/mcb/][Mathematical Components]] by Assia Mahboubi and Enrico Tassi
 - [[https://www.morikita.co.jp/books/book/3287][Formal Proof using Coq/SSReflect/MathComp: Start Formalization of Mathematics with Free Software]] by Manabu Hagiwara and Reynald Affeldt (in Japanese, 日本語)
 - [[http://ilyasergey.net/pnp/][Programs and Proofs: Mechanizing Mathematics with Dependent Types]] by Ilya Sergey
 
-* Introductions
-- [[https://github.com/math-comp/math-comp/wiki/tutorial-itp2016][ITP 2016 tutorial: Mathematical Components, an Introduction]] by Yves Bertot, Cyril Cohen, Assia Mahboubi, Enrico Tassi and Laurent Théry.
+* @@html: &#128210;@@ SSReflect reference manual
+- [[https://hal.inria.fr/inria-00258384/en][A Small Scale Reflection Extension for the Coq system]] by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
+  + the same [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][htmlized as a part]] of Coq reference manual
+
+* @@html: &#x1F3EB;@@ Lectures
+
+
+** Introductions
+
+- @@html:&#127909;@@ [[https://www.youtube.com/watch?app=desktop&v=taqk6tty8wk][Coq/Rocq tutorial: Ssreflect tactics and the MathComp library]] by Marie Kerjean and Cyril Cohen, 2024-03-26
+- [[https://github.com/math-comp/math-comp/wiki/tutorial-itp2016][ITP 2016 tutorial: Mathematical Components, an Introduction]] by Yves Bertot, Cyril Cohen, Assia Mahboubi, Enrico Tassi, and Laurent Théry.
+- [[https://www.jstage.jst.go.jp/article/jssst/34/2/34_2_64/_pdf][Introduction to Mathematical Components]] by Reynald Affeldt (in Japanese, 日本語), 2016
 - [[http://videos.rennes.inria.fr/Conference-ITP/indexAssiaMahboubiEnricoTassi.html][ITP 2013 tutorial: The Mathematical Components library]] by Assia Mahboubi and Enrico Tassi
-- [[https://www.jstage.jst.go.jp/article/jssst/34/2/34_2_64/_pdf][Introduction to Mathematical Components]] by Reynald Affeldt (in Japanese, 日本語)
-- [[http://jfr.unibo.it/article/view/1979][An introduction to small scale reflection in Coq]] by Georges Gonthier and Assia Mahboubi
-* Lectures
+- [[http://jfr.unibo.it/article/view/1979][An introduction to small scale reflection in Coq]] by Georges Gonthier and Assia Mahboubi, 2010
+
+** Class
+
 - [[https://mathcomp-schools.gitlabpages.inria.fr/2022-12-school/school][MathComp School 2022]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry
 - [[https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/][Coq Winter School 2018-2019 (SSReflect & MathComp)]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
 - [[https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/][Coq Winter School 2017-2018 (SSReflect & MathComp)]] by Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
 - [[https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/][Advanced Coq Winter School 2016 for master students]] by Cyril Cohen, Laurence Rideau, Enrico Tassi, Laurent Théry
-- [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/][Coq/SSReflect/MathComp Tutorial]] by Reynald Affeldt (in Japanese, 日本語)
+- [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/][Coq/SSReflect/MathComp Tutorial]] by Reynald Affeldt (in Japanese, 日本語), 2014-2015
 - [[http://www-sop.inria.fr/manifestations/MapSpringSchool/][International Spring School on Formalization of Mathematics (MAP 2012)]] by Yves Bertot, Assia Mahboubi, Laurence Rideau, Pierre-Yves Strub, Enrico Tassi, Laurent Théry
-* Cheatsheets
+
+* @@html:&#128221;@@ Cheatsheets
 - [[http://www-sop.inria.fr/marelle/math-comp-tut-16/MathCompWS/basic-cheatsheet.pdf][Basic cheat sheet]]
 - [[http://www-sop.inria.fr/marelle/math-comp-tut-16/MathCompWS/cheatsheet.pdf][Advanced cheat sheet]]
 - [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/ssrbool_doc.pdf][ssrbool.v]],
@@ -36,18 +48,13 @@
   [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/finset_doc.pdf][finset.v]],
   [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/fingroup_doc.pdf][fingroup.v]]
 
-* SSReflect Reference manual
-- [[https://hal.inria.fr/inria-00258384/en][A Small Scale Reflection Extension for the Coq system]] by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
-  + the same [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][htmlized as a part]] of Coq reference manual
-
-* Conference videos
-
+* @@html:&#127909;@@ Conference videos
 Georges Gonthier about the Mathematical Components project:
 - [[https://www.youtube.com/watch?v=3ak3N31d8_g][Georges Gonthier: Computer proofs: teaching computers mathematics, and conversely]], ICM 2022, 2022-07-07
 - [[https://www.youtube.com/watch?v=ZNB2ZEFw5Zw][Functional Encodings of Mathematics]], Institut des Hautes Études Scientifiques, 2022-06-15 (in French)
 - [[https://www.youtube.com/watch?v=_NDD_jXGwk8][The Logic of Real Proofs]], Federated Logic Conference, 2018-07-14
 - [[https://www.newton.ac.uk/seminar/17967/][Scaffolds and frames: the MathComp algebra formal library]], Isaac Newton Institute, 2017-07-13
 - [[https://www.microsoft.com/en-us/research/video/proof-engineering-from-the-four-colour-to-the-odd-order-theorem/][Proof Engineering, from the Four Colour to the Odd Order Theorem]], Microsoft, 2016-07-16
 - [[https://www.youtube.com/watch?v=frz6MFt36Gc][Digitizing the Group Theory of the Odd Order Theorem]], Institut Henri Poincaré, 2014-04-22
-- [[https://www.youtube.com/watch?v=yBXGdJw1xBI][the four colour theorem]], RU Computer Science, 2013-01-28
+- [[https://www.youtube.com/watch?v=yBXGdJw1xBI][The four colour theorem]], RU Computer Science, 2013-01-28
 - [[https://www.youtube.com/watch?v=TczaUx0B92M][Mechanizing the Odd Order Theorem: Local Analysis]], Institute for Advanced Study, 2011-01-20