Formal Semantics in Modern Type Theories: Is It Model-theoretic, Proof-theoretic, or Both?
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
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 heories (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.