Thursday 20 June 2019, 16:30, LSV library: Cumulative Types Systems and levels, François Thiré (Deducteam PhD student).

Cumulative Typed Systems (CTS), extend Pure Type Systems with a subtyping relation on universes. We introduce LCTS, a CTS enriched with a notion of level. LCTS has subject reduction (reduction preserves types) but lacks a strong reduction property that levels are also preserved. We show that this strong subject reduction property implies two famous conjectures on CTS: Expansion postponement and the equivalence between explicit and implicit conversion. The former is an open conjecture in the general case for PTS/CTS. The latter has been proved by Siles for PTS only and is still a conjecture for CTS. We rephrase this notion of level using a well-founded order on derivation trees. We show that the existence of such well-founded order implies a type system with the strong subject reduction property. Hence, these two conjectures is a direct consequence of the existence of such well-founded order. Yet, it is not known if such well-founded order exists in general.