Cumulative Types Systems and Levels

Abstract : 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 [5] 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [5 references]  Display  Hide  Download
Contributor : Ivan Scagnetto <>
Submitted on : Friday, June 7, 2019 - 9:48:31 AM
Last modification on : Wednesday, December 4, 2019 - 1:30:03 PM


Files produced by the author(s)


  • HAL Id : hal-02150179, version 1


François Thiré. Cumulative Types Systems and Levels. LFMTP 2019 - Logical Frameworks and Meta-Languages: Theory and Practice, Jun 2019, Vancouver, Canada. ⟨hal-02150179⟩



Record views


Files downloads