29th European Summer School in Logic, Language, and Information
University of Toulouse (France), 17-28 July, 2017

Modern Type Theories for Natural Language Semantics

Zhaohui Luo

Language and Logic (Introductory)

Second week, from 11:00 to 12:30


Modern Type Theories (MTTs) provide us with a new framework for formal semantics with attractive advantages as compared to Montague Grammar. First, MTTs have rich type structures that can be employed effectively to capture various linguistic features that have proved difficult in the Montagovian setting. Second, MTTs are proof-theoretically specified and can hence be usefully implemented in proof assistants such as Coq, where the MTT-semantics has been implemented for computer-assisted reasoning. These two respects may be characterised as saying that the MTT-semantics is both model-theoretic and proof-theoretic. They offer unique features unavailable in traditional logical systems that have proved very useful in formal semantics.

We shall introduce MTTs and how they can be used for formal semantics. The lectures will be informal and explanatory. They will be rigorous but contain a lot of examples, to illustrate the use of MTTs, on the one hand, and to compare the MTT-semantics with Montague Grammar, on the other. They should be suitable for any semantics-oriented linguists and the others who can gain from learning a new framework of formal semantics.