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 (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

翻译：我们从线性组合代数出发，构造了一个线性依赖类型理论的实现性模型。该模型为类型理论提出了一系列扩展方案。特别地，我们引入了一个具有两种解码操作的宇宙：一种将编码映射为笛卡尔类型，另一种将编码映射为线性类型。该宇宙在非直谓性意义下是封闭的，因为它同时支持大型笛卡尔依赖积和大型线性依赖积的构造。我们还增加了一条关于模态单射性的规则，该模态可将线性项转化为笛卡尔项。通过这些扩展，我们能够编码（线性）归纳类型。作为案例研究，我们考察了线性类型上的列表类型，并证明我们的编码方案满足相应的唯一性原理。该实现性模型的构造已在证明辅助工具Rocq中完成形式化验证。