MTT-semantics Is Both Model-theoretic and Proof-theoretic

• Event: Seminar
• Lecturer: Zhaohui Luo
• Date: 27 April 2016
• Duration: 2 hours
• Venue: Gothenburg

Abstract:

In this talk, after briefly introducing the formal semantics in modern type theories (MTT-semantics), I shall argue that it is both model-theoretic and proof-theoretic. This is due to the unique features of MTTs: they contain rich type structures that provide powerful representational means (e.g., to represent collections as types) and, at the same time, are specified proof-theoretically as rule-based systems whose sentences (judgements) can be understood inferentially.

Considered in this way, MTTs arguably have promising advantages when employed as foundational languages for formal semantics, both theoretically and practically.

Lecturer:

Zhaohui Luo is a Professor of Computer Science at Royal Holloway, University of London.