Linear typed $\lambda$-calculi are more delicate than their simply typed siblings when it comes to metatheoretic results like preservation of typing under renaming and substitution. Tracking the usage of variables in contexts places more constraints on how variables may be renamed or substituted. We present a methodology based on linear algebra over semirings, extending McBride's kits and traversals approach for the metatheory of syntax with binding to linear usage-annotated terms. Our approach is readily formalisable, and we have done so in Agda.

翻译：线性打字 $\ lambda$- calculi 比简单的打字兄弟姐妹在超理论结果方面更为微妙,比如在重命名和替换下保存打字。跟踪背景中变量的使用情况对变量的重新命名或替换设置了更多的限制。我们提出了一个基于线性代数的半边线性代数的方法,扩大了McBride的套件和跨行法,用于对线性用词附加说明的术语具有约束力的超语法的元理论。我们的方法很容易正规化,我们在Agda也这样做了。