[MLTT resources]
The original notes: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf
A formal overview: https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory
Another denoscription: http://www.cse.chalmers.se/~peterd/papers/IntuitionisticTypeTheory150505.pdf
Programming in Martin-Löf type theory: https://www.dimap.ufrn.br/~regivan/pub/Programming_In_Martin_Loef_Type_Theory.pdf
[Resources for MLTT or similar about specific languages:]
Logic and Proof in Lean: https://leanprover.github.io/logic_and_proof/
General Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/
Programming Language Foundations in Agda: https://plfa.github.io/
Software foundations (based on Coq): https://softwarefoundations.cis.upenn.edu/current/index.html
The Nuprl Proof Development System: http://www.nuprl.org/book/
[HoTT resources]
The HoTT Book: https://homotopytypetheory.org/book/
HoTT in Agda: https://github.com/HoTT/HoTT-Agda
HoTT in Coq: https://github.com/HoTT/HoTT
The CoqHoTT project: http://coqhott.gforge.inria.fr/
Cubical type theory: https://arxiv.org/abs/1611.02108
Cubical type theory as Agda extension: https://agda.readthedocs.io/en/latest/language/cubical.html
Cubical Agda library: https://github.com/agda/cubical
The main implementation: https://github.com/mortberg/cubicaltt
An introduction to cubicaltt: https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/

A type checker for a modal dependently typed theory
https://github.com/jozefg/blott
[Thanks to clayrat]

A proof checker for cartesian cubical type theory
https://github.com/RedPRL/redtt
This goes even beyond the generality of cubical type theory, since paths are defined by even more general cube boundaries.
[Thanks to Brett]

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