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.

翻译：我们提出了一个第一阶语法下 lambda 演算形式元理论的框架，其中包含两种名称，一种用于表示自由和绑定变量，另一种用于常量，并使用 Stoughton 的多重代换。在该框架之上，我们证明了简单类型 lambda 演算和 System T 的 Girard 强正则化定理。对于后者，我们还展示了原始证明的简化。整个开发过程都是使用 Agda 系统进行机器检查的。