Intrinsically Typed Syntax See here for the final PDFs of the Thesis and for the presentation slides.