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.

I also made a group for discussion about resources/this channel's topics:
@typetheorygroup

BPF and formal verification
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]

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..

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.

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