In this talk, I will discuss the use of Modern Type Theoretical Semantics (MTTs) , i.e. type theories within the tradition of Martin Löf (1974, 1981), for reasoning about natural language semantics. I will first present a brief introduction of the features that make MTTs an attractive formal language to interpret NL semantics to. In particular, I will discuss a number of issues that have been successfully dealt with using MTTs like adjectival/adverbial modification, copredication and intensionality among other things. Then, I will argue that the proof-theoretic nature of MTTs, i.e. the fact that they are proof-theoretically specified, in combination with their expresiveness makes them fit to perform reasoning tasks. This proof-theoretic aspect of MTTs has been the main reason that a number of proof-assistants implement variants of MTTs. One such proof-assistant, Coq, will be used as a way to show the applicability of MTTs in dealing with Natural Language Inference (NLI). Firstly, I will show how NL semantics can be implemented in Coq and then I will present how one can use Coq in order to reason with these semantics. I will draw examples from the FraCas test suite platform in order to show the predictions the implemented semantics make as regards inference. I will then discuss issues like coverage and proof-automation and a number of ideas for future work, like extracting type ontologies from GWAP lexical networks and creating a parser/translator that will translate between English (or any other language) and the syntax of Coq.