Mechanical proofs by logical relations often involve tedious reasoning about substitution. In this paper, we show that this is not necessarily the case, by developing, in Agda, a proof that all simply typed lambda calculus expressions evaluate to values. A formalization of the proof is remarkably short (~40 lines of code), making for an excellent introduction to the technique of proofs by logical relations not only on paper but also in a mechanized setting. We then show that this process extends to more sophisticated reasoning by also proving the totality of normalization by evaluation. Although these proofs are not new, we believe presenting them will empower both new and experienced programming language theorists in their use of logical relations.

翻译：通过逻辑关系进行的机械化证明常常需要关于替换的繁琐推理。在本文中，我们通过在Agda中开发一个证明，表明所有简单类型λ演算表达式都能求值为值，从而证明情况并非必然如此。该证明的形式化过程异常简洁（约40行代码），使其不仅能在纸面上，还能在机械化环境中成为逻辑关系证明技术的绝佳入门示例。随后，我们展示这一过程可以扩展到更复杂的推理，同时证明了通过求值进行规范化的总体性。尽管这些证明并非全新，但我们相信，呈现它们将能帮助新的和经验丰富的编程语言理论家更好地运用逻辑关系。