Quantitative type theory (QTT) is an extension of dependent type theory which allows us to track the number of computational (non-erased) uses of variables in well-typed lambda terms. With such usage information, QTT allows us to combine dependent types with substructural types, such as linear, affine or relevant types.
While in a Martin-Löf style type theory typing judgments are of form
x1 : A1, ..., xn : An ⊢ b : B, in QTT the bindings in the context