I also made a group for discussion about resources/this channel's topics:
@typetheorygroup
@typetheorygroup
BPF and formal verification
https://www.sccs.swarthmore.edu/users/16/mmcconv1/pl-reflection.html
[Thanks to parra]
https://www.sccs.swarthmore.edu/users/16/mmcconv1/pl-reflection.html
[Thanks to parra]
[Some kind of selfadvertisement]
I also got a blog where I'll post entries about type theory and similar things on some rare occasion: logicandtypes.org
[End of advertisement]
I also got a blog where I'll post entries about type theory and similar things on some rare occasion: logicandtypes.org
[End of advertisement]
From design patterns to category theory
https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/
Reusing abstraction that exists for several decades..
https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/
Reusing abstraction that exists for several decades..
ploeh blog
From design patterns to category theory
How do you design good abstractions? By using abstractions that already exist.
Introductions on Topology
http://pi.math.cornell.edu/~matsumura/math4530/IntroToTopology.pdf
https://www.math.colostate.edu/~renzo/teaching/Topology10/Notes.pdf
https://math.bme.hu/~kalex/Teaching/Spring10/Topology/TopNotes_Spring10.pdf
This is not directly related, but it might be considered useful.
http://pi.math.cornell.edu/~matsumura/math4530/IntroToTopology.pdf
https://www.math.colostate.edu/~renzo/teaching/Topology10/Notes.pdf
https://math.bme.hu/~kalex/Teaching/Spring10/Topology/TopNotes_Spring10.pdf
This is not directly related, but it might be considered useful.
Proofs are programs: 19th century logic and 21st century computing
"For my money, Gentzen’s natural deduction and Church’s lambda calculus are on a par with Einstein’s relativity and Dirac’s quantum physics for elegance and insight. And the maths are a lot simpler." - Wadler, 2000.
https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
"For my money, Gentzen’s natural deduction and Church’s lambda calculus are on a par with Einstein’s relativity and Dirac’s quantum physics for elegance and insight. And the maths are a lot simpler." - Wadler, 2000.
https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
A Monoid Is a Category With Just One Object. So What's the Problem?
https://k-bx.github.io/articles/boring-monoid-category.html
An introduction on category theory as well as on proof assistants.
[Thanks to Brett]
https://k-bx.github.io/articles/boring-monoid-category.html
An introduction on category theory as well as on proof assistants.
[Thanks to Brett]
What is a Natural transformation?
https://www.math3ma.com/blog/what-is-a-natural-transformation
https://www.math3ma.com/blog/what-is-a-natural-transformation
Math3Ma
What is a Natural Transformation? Definition and Examples
I hope you have enjoyed our little series on basic category theory. (I know I have!) This week we'll close out by chatting about natural transformations which are, in short, a nice way of moving from one functor to another. If you're new to this mini-series…
Computational higher type theory
https://arxiv.org/abs/1604.08873
https://arxiv.org/abs/1604.08873
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.