Has cool tutorials and materials on software verification, category theory, type theory foundations, programming in agda, certified programming and state, proof theory, designing your own dependently typed programming language, and software foundations in Coq.

Has cool tutorials and materials on software verification, category theory, type theory foundations, programming in agda, certified programming and state, proof theory, designing your own dependently typed programming language, and software foundations in Coq.

I’m particularly interested in Weirich’s dependently typed PL exercise here: https://github.com/sweirich/pi-forall

The series on designing a dependently typed language looks pretty interesting.