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.