Skip to content

Commit b2ceb68

Browse files
authored
book and videos about HB and mc-analysis (#125)
* book and videos about HB and mc-analysis
1 parent e323942 commit b2ceb68

2 files changed

Lines changed: 104 additions & 42 deletions

File tree

documentation.html

Lines changed: 99 additions & 40 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

documentation.org

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@
1414
- [[https://math-comp.github.io/mcb/][Mathematical Components]] by Assia Mahboubi and Enrico Tassi
1515
- [[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, 日本語)
1616
- [[http://ilyasergey.net/pnp/][Programs and Proofs: Mechanizing Mathematics with Dependent Types]] by Ilya Sergey
17-
17+
- [[https://staff.aist.go.jp/reynald.affeldt/documents/karate-rocq.pdf][Karate-Coq, An Introduction to MathComp-Analysis]] by Reynald Affeldt
1818
* @@html: 📒@@ SSReflect reference manual
1919
- [[https://hal.inria.fr/inria-00258384/en][A Small Scale Reflection Extension for the Coq system]] by Georges Gonthier, Assia Mahboubi, and Enrico Tassi
2020
+ the same [[https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html][htmlized as a part]] of Coq reference manual
@@ -49,7 +49,10 @@
4949
[[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/fingroup_doc.pdf][fingroup.v]]
5050

5151
* @@html:🎥@@ Conference videos
52-
Georges Gonthier about the Mathematical Components project:
52+
- [[https://www.youtube.com/watch?v=v5hNHr7CF3Q][An Overview of MathComp-Analysis and Its Applications]] by Reynald Affeldt at the Rocqshop 2025
53+
- [[https://www.youtube.com/watch?v=NJetR3C6uH8][Building Measure Theory using Hierarchy Builder]] by Cyril Cohen at the Hausdorff Center for Mathematics, 2024
54+
55+
** Georges Gonthier about the Mathematical Components project:
5356
- [[https://www.youtube.com/watch?v=3ak3N31d8_g][Georges Gonthier: Computer proofs: teaching computers mathematics, and conversely]], ICM 2022, 2022-07-07
5457
- [[https://www.youtube.com/watch?v=ZNB2ZEFw5Zw][Functional Encodings of Mathematics]], Institut des Hautes Études Scientifiques, 2022-06-15 (in French)
5558
- [[https://www.youtube.com/watch?v=_NDD_jXGwk8][The Logic of Real Proofs]], Federated Logic Conference, 2018-07-14

0 commit comments

Comments
 (0)