My solutions to the excellent class on type theory and formal verification (INF551) taught by Samuel Mimram at the Ecole Polytechnique in 2018: INF551 – Computational logic: from Artificial intelligence to Zero bugs
The class is now available as a book, called Program = Proof. I highly recommend it.
Code in either OCaml or Agda.