An introduction to category theory
http://www.cs.man.ac.uk/~hsimmons/zCATS.pdf
Note that this one seemed pretty simple and not that formal to me, compared to many others.

A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
http://io.livecode.ch/learn/namin/icfp2017-artifact-auas7pp
An introduction to logic- and metaprogramming using Scheme, while showing true test-driven development.

Asymptotically, almost all Lambda-Terms are strongly normalizing
https://arxiv.org/pdf/0903.5505.pdf
This paper shows that almost all lambda terms are strongly normalizing, while for combinatory logic, the opposite applies.

To be precise, the lower bound for normalizing lambda terms of size n is ((4 - eps) * n/ln(n))^(n-(n/ln(n))), where eps is between 0 and 4.

The upper bound for such terms is ((12 + eps)*n/ln(n))^(n-(n/(3*ln(n))) for any eps > 0.

Syntax and Semantics of Quantitative Type Theory
https://bentnib.org/quantitative-type-theory.pdf
A type theory recording usage information for variables, which lead to even better denoscriptions by types
[Thanks to trevthedev, check out his channel @thevikingprogrammer]

Is the law of the excluded middle true?
http://www.grall.name/posts/2/excludedMiddle-trueFalse.html
Proving a weak form of the law of the excluded middle false by proving the undecidability of the halting problem.

Subminimal logic
https://dspace.jaist.ac.jp/dspace/bitstream/10119/15191/5/paper.pdf
[Thanks to no_identd]

Codata types and Copattern matching
https://www.cl.cam.ac.uk/events/metaprog/2016/codata-types-and-copattern-matching.pdf
Well-defined, inverse pattern matching defining the behavior of destructors applied on function results.

Computational Quadrinitarianism (Curious Correspondences go Cubical)
http://comonad.com/reader/2018/computational-quadrinitarianism-curious-correspondences-go-cubical/
The quadrinity of logic, languages, categories and spaces.
[Thanks to no_identd]

Unison
https://github.com/unisonweb/unison
A language supporting transfer of computation

Lenses from Scratch
An introduction to lenses in Haskell.
https://github.com/ajnsit/haskell-tutorials/blob/master/lenses-from-scratch.md

Cosette: An Automated SQL Solver
http://cosette.cs.washington.edu/
...checking the equivalence of queries and written using HoTT.

Math computation (?)
http://math-comp.github.io
A giant coq library for practical mathematics.

Physics, Topology, Logic, Computation
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.