Computational Type Theory by Robert Harper (2018)

Higher Inductive Types in Cubical Computational Type Theory (2019)

JonPRL - Proof refinement logic for computational type theory based on realizability & the verificationist meaning explanation.