Seven sketches in composability
http://math.mit.edu/~dspivak/teaching/sp18/
http://math.mit.edu/~dspivak/teaching/sp18/
math.mit.edu
Seven Sketches in Compositionality
Category theory is a relatively new branch of mathematics that has
transformed much of pure math research. The technical advance is that
category theory provides a framework in which to organize formal systems
and by which to translate between them, allowing…
transformed much of pure math research. The technical advance is that
category theory provides a framework in which to organize formal systems
and by which to translate between them, allowing…
The Catsters' category theory videos
https://www.youtube.com/playlist?list=PLlGXNwjYhXYxKVa67r0pKuYufECy713bv
https://www.youtube.com/playlist?list=PLlGXNwjYhXYxKVa67r0pKuYufECy713bv
YouTube
The Catsters' Category Theory Videos - YouTube
Type-driven development in Idris
https://www.manning.com/books/type-driven-development-with-idris
A practical programming language with dependent types.
https://www.manning.com/books/type-driven-development-with-idris
A practical programming language with dependent types.
Manning Publications
Type-Driven Development with Idris - Edwin Brady
Write safer, faster code! Learn type-driven development with Idris, from the language's creator.
Functional design and architecture
https://graninas.com/functional-design-and-architecture-book/
https://graninas.com/functional-design-and-architecture-book/
Inside a Black Hole
Functional Design and Architecture: Examples in Haskell (Manning Publications)
FDaA: EH is an advanced book about building real programs with an engineering approach in statically typed functional languages. Buy here: Functional Design and Architecture: Example in Haskell It …
Sets, Logic, Computation
http://builds.openlogicproject.org/courses/phil379/phil379-screen.pdf
http://builds.openlogicproject.org/courses/phil379/phil379-screen.pdf
The Rascal Metaprogramming language
https://www.rascal-mpl.org/
https://www.rascal-mpl.org/
Agda base
https://github.com/pcapriotti/agda-base/tree/master/src
A Agda library with HoTT support, not requiring cubical anything, which is simple and runs on any modern agda version, unlike HoTT-Agda.
https://github.com/pcapriotti/agda-base/tree/master/src
A Agda library with HoTT support, not requiring cubical anything, which is simple and runs on any modern agda version, unlike HoTT-Agda.
GitHub
pcapriotti/agda-base
Base library for HoTT in Agda. Contribute to pcapriotti/agda-base development by creating an account on GitHub.
Structuralism, Invariance, and Univalence
https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
Kind of an introduction to HoTT.
[Thanks to Brett]
https://www.andrew.cmu.edu/user/awodey/preprints/siu.pdf
Kind of an introduction to HoTT.
[Thanks to Brett]
Unintentional type theory
http://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf
(for those people who haven't noticed it so far, this is a joke)
http://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf
(for those people who haven't noticed it so far, this is a joke)
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
https://arxiv.org/abs/1301.3443
https://arxiv.org/abs/1301.3443
Foundations of Software Science and Computation Structures
https://link.springer.com/book/10.1007%2F978-3-319-89366-2
https://link.springer.com/book/10.1007%2F978-3-319-89366-2
Springer
Foundations of Software Science and Computation Structures | SpringerLink
This book is Open Access under a CC BY licence.
To be or not to be constructive, that is not the question
https://arxiv.org/abs/1704.00462
https://arxiv.org/abs/1704.00462
arXiv.org
To be or not to be constructive, that is not the question
In the early twentieth century, L.E.J. Brouwer pioneered a new philosophy of
mathematics, called intuitionism. Intuitionism was revolutionary in many
respects but stands out -mathematically...
mathematics, called intuitionism. Intuitionism was revolutionary in many
respects but stands out -mathematically...
A synthetic theory of infinity-categories in homotopy type theory
http://www.math.jhu.edu/~eriehl/octoberfest.pdf
http://www.math.jhu.edu/~eriehl/octoberfest.pdf
Applied Category Theory conference
https://www.youtube.com/user/wires0/live
Note that this is a livestream.
https://www.youtube.com/user/wires0/live
Note that this is a livestream.
YouTube
Jelle Herold
... and its programme, thanks to Daniele.
Forwarded from Daniele
ACT 2019 programme.pdf
304.2 KB