Lenses from Scratch
An introduction to lenses in Haskell.
https://github.com/ajnsit/haskell-tutorials/blob/master/lenses-from-scratch.md
An introduction to lenses in Haskell.
https://github.com/ajnsit/haskell-tutorials/blob/master/lenses-from-scratch.md
GitHub
ajnsit/haskell-tutorials
Lens is the new Monad. Contribute to ajnsit/haskell-tutorials development by creating an account on GitHub.
Setoid type theory
https://akaposi.github.io/brutal.pdf
https://akaposi.github.io/brutal.pdf
Cosette: An Automated SQL Solver
http://cosette.cs.washington.edu/
...checking the equivalence of queries and written using HoTT.
http://cosette.cs.washington.edu/
...checking the equivalence of queries and written using HoTT.
Physics, Topology, Logic, Computation
https://arxiv.org/pdf/0903.0340.pdf
The quintuplity (?) of Hilbert spaces, logics, topological spaces, categories, and languages.
https://arxiv.org/pdf/0903.0340.pdf
The quintuplity (?) of Hilbert spaces, logics, topological spaces, categories, and languages.
Other groups/channels I'd like to share
Note that I won't use @tags to prevent scraping, just put them at the beginning.
deepspec - A group exactly about this channel's topics such as type theory and program verification.
@logicprogrammingchan - an inactive channel that is more focused on programming in general, however not about mainstream languages but rather FP/LP and Forth.
gnugroup - about free software and a bit of general talk
emacs_en - for discussion about the superior editor
nixos_en - GuixSD and NixOS, GNU/Linux distributions with stateless package managers and great noscripting capabilities
@thevikingprogrammer - a channel about programming, but also sharing general things and stuff
Shoutout to trev, brett, cornburglar and sven (who will not read this because he switched to matrix) for introducing me to several concepts and making things like this even possible. Thanks.
Note that I won't use @tags to prevent scraping, just put them at the beginning.
deepspec - A group exactly about this channel's topics such as type theory and program verification.
@logicprogrammingchan - an inactive channel that is more focused on programming in general, however not about mainstream languages but rather FP/LP and Forth.
gnugroup - about free software and a bit of general talk
emacs_en - for discussion about the superior editor
nixos_en - GuixSD and NixOS, GNU/Linux distributions with stateless package managers and great noscripting capabilities
@thevikingprogrammer - a channel about programming, but also sharing general things and stuff
Shoutout to trev, brett, cornburglar and sven (who will not read this because he switched to matrix) for introducing me to several concepts and making things like this even possible. Thanks.
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...