diff --git a/documentation.html b/documentation.html index 2e2a3350..cea6e7f1 100644 --- a/documentation.html +++ b/documentation.html @@ -3,14 +3,14 @@ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - + Mathematical Components: Documentation - + @@ -199,60 +199,13 @@ - -
+

Mathematical Components: Documentation

- -
-

Books

-
+
+

📚 Books

+
- -
-

Introductions

-
+
+

📒 SSReflect reference manual

+
+ +
+
+
+

🏫 Lectures

+
+
+
+

Introductions

+
-
-

Lectures

-
+
+

Class

+
-
-

Cheatsheets

-
+
+
+

📝 Cheatsheets

+
- -
-

SSReflect Reference manual

-
- -
-
- -
-

Conference videos

-
+
+

🎥 Conference videos

+

Georges Gonthier about the Mathematical Components project:

@@ -325,7 +281,7 @@

Conference videos

  • Scaffolds and frames: the MathComp algebra formal library, Isaac Newton Institute, 2017-07-13
  • Proof Engineering, from the Four Colour to the Odd Order Theorem, Microsoft, 2016-07-16
  • Digitizing the Group Theory of the Odd Order Theorem, Institut Henri Poincaré, 2014-04-22
    • -
  • the four colour theorem, RU Computer Science, 2013-01-28
    • +
  • The four colour theorem, RU Computer Science, 2013-01-28
  • Mechanizing the Odd Order Theorem: Local Analysis, Institute for Advanced Study, 2011-01-20
    • diff --git a/documentation.org b/documentation.org index 8d4efd57..860d7ef6 100644 --- a/documentation.org +++ b/documentation.org @@ -10,24 +10,36 @@ #+HTML_HEAD: #+HTML_HEAD: -* Books +* @@html:📚@@ 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: 📒@@ 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: 🏫@@ Lectures + + +** Introductions + +- @@html:🎥@@ [[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:📝@@ 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,12 +48,7 @@ [[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:🎥@@ 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) @@ -49,5 +56,5 @@ Georges Gonthier about the Mathematical Components project: - [[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