Foundations in Coq - formalizing my undergraduate coursework
Coq
0
1 commits
updated Nov 6, 2024
README
Foundations in Coq
An attempt to formalize undergraduate mathematics into type theory, in real time as I learn it.
Textbooks:
- Calculus, Apostol
- Linear Algebra Done Right, Axler
- Elementary Differential Equations and Boundary Value Problems, Boyce and DiPrima
- Contemporary Abstract Algebra, Gallian
- An Introduction to Categories and Sheaves, Schapira
References:
- https://softwarefoundations.cis.upenn.edu/
- https://arxiv.org/abs/1102.1323
- https://github.com/coq-community/corn
- https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html
- http://adam.chlipala.net/cpdt/html/MoreDep.html
- https://inria.hal.science/hal-00816703v1/document
- https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt/karate-coq-nagoya2022.pdf
- https://unimath.github.io/bham2017/uf.pdf
- https://webusers.imj-prg.fr/~pierre.schapira/LectNotes/CatShv.pdf
Contributors
lukeearly
1 commits
Similar repos
Languages
Coq
96.4%
V
3.6%
Foundations in Coq - formalizing my undergraduate coursework
Coq
0
1 commits
updated Nov 6, 2024
README
Foundations in Coq
An attempt to formalize undergraduate mathematics into type theory, in real time as I learn it.
Textbooks:
- Calculus, Apostol
- Linear Algebra Done Right, Axler
- Elementary Differential Equations and Boundary Value Problems, Boyce and DiPrima
- Contemporary Abstract Algebra, Gallian
- An Introduction to Categories and Sheaves, Schapira
References:
- https://softwarefoundations.cis.upenn.edu/
- https://arxiv.org/abs/1102.1323
- https://github.com/coq-community/corn
- https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html
- http://adam.chlipala.net/cpdt/html/MoreDep.html
- https://inria.hal.science/hal-00816703v1/document
- https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt/karate-coq-nagoya2022.pdf
- https://unimath.github.io/bham2017/uf.pdf
- https://webusers.imj-prg.fr/~pierre.schapira/LectNotes/CatShv.pdf
Similar repos
Contributors
lukeearly
1 commits
Languages
Coq
96.4%
V
3.6%