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

https://hal.archives-ouvertes.fr/hal-02150179
Contributor : Ivan Scagnetto <>
Submitted on : Friday, June 7, 2019 - 9:48:31 AM
Last modification on : Tuesday, October 15, 2019 - 2:50:38 PM

File

LFMTP2019_SP_1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02150179, version 1

Citation

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

Share

Metrics

Record views

63

Files downloads

51