论文标题
线性代数方法的线性元学方法
A Linear Algebra Approach to Linear Metatheory
论文作者
论文摘要
线性键入$λ$ -calculi在元心he镜结果（例如保存在重命名和替代下打字）时简单地打字的兄弟姐妹更精致。在上下文中跟踪变量的使用情况对变量的重命名或替换更大。我们提出了一种基于线性代数的方法论，在半半段上扩展了McBride的套件和遍历语法的介质方法，并结合了线性使用的术语。我们的方法很容易形式化，我们在AGDA中这样做。
Linear typed $λ$-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.
