{"id":"arxiv/2602.08846","url":"https://arxiv.org/abs/2602.08846","tags":["cs.LO","cs.PL","math.CT","math.LO"],"score":0,"title":"Impredicativity in Linear Dependent Type Theory","domain":"cs.LO","source":"arxiv","authors":["Sam Speight","Niels van der Weide"],"reviews":0,"subject":"cs.LO","summary":"We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-09","reactions":{}}