Impredicativity in Linear Dependent Type Theory

TL;DR

This paper develops a realizability model for linear dependent type theory with an impredicative universe, enabling encoding of inductive types and formal verification in Rocq.

Contribution

It introduces a realizability model with an impredicative universe supporting both cartesian and linear dependent products, and formalizes it in Rocq.

Findings

Successfully encodes linear inductive types.

Demonstrates the universe's impredicativity with large dependent products.

Provides a formal proof in Rocq.

Abstract

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.