Formal Semantics in Modern Type Theories: Theory and Implementation
Stergios Chatzikyriakidis & Zhaohui Luo
Language & Logic
Week Two - 14.00-15.30 - Level: A
Formal semantics based on Modern Type Theories (MTTs) provides us not only with a viable alternative to Montague Grammar, but potentially with an attractive full-blown semantic tool with advantages in many respects, both theoretically and computationally. In this course, we shall introduce the MTT-semantics and then use it to study several semantic issues such as adjectival/adverbial modification, co-predication, coordination and belief intensionality among others.
Key comparisons to Montague Grammar are done all along, discussing the advantages of MTTs over simple type theory. For example, subtyping is crucially needed for proper semantic treatments of some linguistic features but has proven difficult in a Montagovian setting. The employment of coercive subtyping solves this problem for MTT-semantics: it is adequate for MTTs and has been shown to be a key foundation in MTT semantics.
MTTs have been implemented in proof assistants (e.g., Agda, Coq, LEGO, Plastic), which can be used to implement MTT-based semantics and hence conduct computer-assisted reasoning in natural language. We shall consider NL inference implemented in Coq to show that such activities can be supported effectively.
For this course, the basic knowledge of Montague Grammar is useful, although not necessary.