The elements of an inductive type
http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/
http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/
Approximate Normalization for Gradual Dependent Types
https://arxiv.org/abs/1906.06469
[OP is Brett, fixed format]
https://arxiv.org/abs/1906.06469
[OP is Brett, fixed format]
Combinatorial Species and Labelled Structures
http://ozark.hendrix.edu/~yorgey/pub/thesis.pdf
http://ozark.hendrix.edu/~yorgey/pub/thesis.pdf
Linear logic for constructive mathematics
https://arxiv.org/abs/1805.07518
https://arxiv.org/abs/1805.07518
arXiv.org
Affine logic for constructive mathematics
We show that numerous distinctive concepts of constructive mathematics arise automatically from an "antithesis" translation of affine logic into intuitionistic logic via a Chu/Dialectica...
nevermind, posted this before
Cartesian Cubical computational type theory
https://hott-uf.github.io/2018/slides/FavoniaHoTTUF2018.pdf
https://hott-uf.github.io/2018/slides/FavoniaHoTTUF2018.pdf
Univalent foundations
https://www.ias.edu/ideas/2014/voevodsky-foundations-video
https://www.ias.edu/ideas/2014/voevodsky-foundations-video
Institute for Advanced Study
Univalent Foundations: New Foundations of Mathematics
In Voevodsky’s experience, the work of a mathematician is 5% creative insight and 95% self-verification. Moreover, the more original the insight, the more one has to pay for it later in self-verification work. The Univalent Foundations project, started at…
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...