Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and logical relations are common patterns of such inductive constructions. They allow representing the translation and the proofs of the invariants as a set of translation rules, corresponding to the cases of the inductions. Importantly, establishing the invariants is reduced to checking a finite set of, typically decidable, statements. Therefore, in a framework supporting theory morphisms and logical relations, translations that fit one of these patterns become much easier to formalize and to verify. The $\lambda\Pi$-calculus modulo rewriting is a logical framework designed for representing and translating between formal systems that has previously not systematically supported such patterns. In this paper, we extend it with theory morphisms and logical relations. We apply these to define and verify invariants for a number of translations between formal systems. In doing so, we identify some best practices that enable us to obtain elegant novel formalizations of some challenging translations, in particular type erasure translations from typed to untyped languages.

翻译：形式系统的表示定理通常采用满足特定不变量的归纳翻译形式，这些不变量通过归纳法证明。理论态射与逻辑关系是此类归纳构造的常见模式。它们允许将翻译及不变量的证明表示为一组翻译规则，对应于归纳的各个情形。重要的是，建立不变量被简化为检查一组有限且通常可判定的陈述。因此，在支持理论态射与逻辑关系的框架中，符合这些模式的翻译将变得更容易形式化与验证。$\lambda\Pi$-演算模重写是一种专为形式系统表示与翻译设计的逻辑框架，此前并未系统支持此类模式。本文通过引入理论态射与逻辑关系对该框架进行扩展。我们运用这些工具为多个形式系统间的翻译定义并验证不变量。在此过程中，我们总结出若干最佳实践，从而实现了对某些具有挑战性翻译的优雅新颖形式化，特别是从类型化语言到无类型语言的类型擦除翻译。