Note that the used logic is equivalent to one only using Ax 1,2,3, as long as you have a notion of assumption.

The incredible proof machine
http://incredible.pm/
Some kind of proof playground to start off.

Guarded computational type theory
https://arxiv.org/abs/1804.09098
A type theory capuring the notion of productivity while being a compuational metalanguage.
[Thanks to petercommand]

[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]