We present a framework for the formal meta-theory of lambda calculi in first-order syntax, with two sorts of names, one to represent both free and bound variables, and the other for constants, and by using Stoughton's multiple substitutions. On top of the framework we formalize Girard's proof of the Strong Normalization Theorem for both the simply-typed lambda calculus and System T. As to the latter, we also present a simplification of the original proof. The whole development has been machine-checked using the Agda system.

翻译：我们提出一个用于一阶语法中λ演算形式元理论框架，该框架引入两类名称——一类同时表示自由变量和约束变量，另一类表示常量——并采用Stoughton多重替换机制。在此框架基础上，我们形式化了Girard关于简单类型λ演算和System T的强规范化定理证明，针对后者还提出了对原始证明的简化方案。整套形式化开发已通过Agda系统完成机器检验。