Formal Semantics in Modern Type Theories

Modern Type Theories (MTTs), (type theories within the tradition of Martin-Löf,) have been shown to be a serious alternative to set theory in the study of mathematical foundations and have been furthermore shown to be the most suited logical languages to perform reasoning tasks. In linguistics, modern type theories have been relatively unknown, the exception being Ranta’s pioneering book more than 20 years ago and sparse papers on the issue ever since. Based on work by the authors and colleagues in recent years, this book takes the challenge to propose to use MTTs as an alternative framework for Natural Language semantics, providing foundational languages that are considerably rich, computationally attractive and foremost well-suited to perform reasoning with NL semantics tasks.