合作交流 / 学术报告

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
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 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.