Till startsida
University of Gothenburg
To content Read more about how we use cookies on gu.se

Zhaohui Luo "Universes in MTT-semantics"

Research profile seminar

Zhaohui Luo "Universes in MTT-semantics"

In type theory, a universe is a type of types. Universes play important roles when modern type theories (MTTs) are employed as foundational languages for linguistis semantics. In this talk, I'll report work on two kinds of universes in the study of MTT-semantics. The first kind may be called linguistic universes which include CN, the universe of common nouns, and LType, the universe employed in the study of coordination. It is shown how they are introduced and used in semantic studies and, in particular, their usefulness is reflected in how they facilitate \Pi-polymorphism in various semantic formalisations.

I shall then study logical universes. In order to formulate MTT-semantics adequately, proof irrelevance needs to be enforced in the underlying type theory. For example, in type theory UTT, this is possible because there is the universe Prop of all logical propositions. However, in Martin-Löf's type theory, this is impossible because types and propositions are identified in MLTT. I propose that the extension of MLTT with h-logic, as developed in the HoTT project, can be used adequately as a foundational language for MTT-semantics, since there is a built-in notion of proof irrelevance in h-logic.

Lecturer: Zhaohui Luo

Date: 12/3/2018

Time: 1:15 PM - 3:00 PM

Categories: Linguistics

Organizer: CLASP

Location: Department of Philosophy, Linguistics and Theory of Science
T346, Olof Wijksgatan 6

Contact person: Stergios Chatzikyriakidis


To the calendar

Page Manager: Stergios Chatzikyriakidis|Last update: 5/23/2016

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?