An inquiry into the Foundations of Mathematics
https://artagnon.com/articles/fom
https://artagnon.com/articles/fom
Artagnon
artagnon.com: articles/fom
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
https://ris.utwente.nl/ws/portalfiles/portal/6142049/meijer91functional.pdf
https://ris.utwente.nl/ws/portalfiles/portal/6142049/meijer91functional.pdf
Typer: ML boosted with type theory and Scheme https://www.iro.umontreal.ca/~monnier/typer-jfla2019.pdf
Understanding F-Algebras
https://www.schoolofhaskell.com/user/bartosz/understanding-algebras
https://www.schoolofhaskell.com/user/bartosz/understanding-algebras
Code and resources for "Handbook of Practical Logic and Automated Reasoning"
https://www.cl.cam.ac.uk/~jrh13/atp/
https://www.cl.cam.ac.uk/~jrh13/atp/
It Is What It Is (And Nothing Else) | Existential Type
https://existentialtype.wordpress.com/2016/02/22/it-is-what-it-is-and-nothing-else/
https://existentialtype.wordpress.com/2016/02/22/it-is-what-it-is-and-nothing-else/
Existential Type
It Is What It Is (And Nothing Else)
A recent discussion of introductory computer science education led to the topic of teaching recursion. I was surprised to learn that students are being taught that recursion requires understanding…
Category Theory for Programmers: OCaml Edition Officially Released
https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1.4.0-rc1
https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1.4.0-rc1
GitHub
Release The OCaml edition! · hmemcpy/milewski-ctfp-pdf
It's here! The first release of the OCaml edition of Category Theory for Programmers!
Huge thanks to @ArulselvanMadhavan for contributing the code snippets!
Huge thanks to @ArulselvanMadhavan for contributing the code snippets!
Clowns to the Left of me, Jokers to the Right
http://strictlypositive.org/CJ.pdf
http://strictlypositive.org/CJ.pdf
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
https://arxiv.org/abs/1803.10228
[Thanks to Elias]
https://arxiv.org/abs/1803.10228
[Thanks to Elias]
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
https://arxiv.org/abs/1509.07584
https://arxiv.org/abs/1509.07584
arXiv.org
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of "adjoint logic" in which the discretization and codiscretization modalities are...
Internal Universes in Models of Homotopy Type Theory
https://arxiv.org/abs/1801.07664
https://arxiv.org/abs/1801.07664
Recovering Purity with Comonads and Capabilities
https://arxiv.org/pdf/1907.07283.pdf
https://arxiv.org/pdf/1907.07283.pdf
Surreal Ordered Exponential Fields
https://arxiv.org/pdf/2002.07739.pdf
https://arxiv.org/pdf/2002.07739.pdf
Non-distributive Logics: From Semantics to Meaning
https://arxiv.org/pdf/2002.04257.pdf
https://arxiv.org/pdf/2002.04257.pdf
Mathematical Structures
http://math.chapman.edu/~jipsen/structures/doku.php
An extremely comprehensive list.
http://math.chapman.edu/~jipsen/structures/doku.php
An extremely comprehensive list.