If you want to read a somewhat longer treatise about dependent types and language, try the book "Modal Homotopy Type Theory". Modal logic has been basically inv

If you want to read a somewhat longer treatise about dependent types and language, try the book "Modal Homotopy Type Theory". Modal logic has been basically invented for linguistic problems. I don't think dependent types are essential for giving language a formal semantics though, I think discourse representation theory has a more direct approach.