Title: Formal Semantics in Modern Type Theories: Is It Model-theoretic, Proof-theoretic, or Both?

Speaker: Zhaohui Luo (University of London, UK)

Time: 14 August 2014, 15:00

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

In this talk, we contend that, for NLs, the divide between model-theoretic semantics and proof-theoretic semantics has not been well-understood. In particular, the formal semantics based on modern type theories (MTTs) may be seen as both model-theoretic and proof-theoretic. To be more precise, the MTT-semantiics may be seen both ways in the sense that the NL semantics can first be represented in an MTT in a model-theoretic way and then the semantic representations can be understood inferentially in a proof-theoretic way. Considered like this, MTTs arguably have unique advantages when employed for formal semantics. We shall first give a brief introduction to the MTT-semantics and its recent development and then turn into the explanations of the above theme.