Formalizing Representation Theorems for a Logical Framework with Rewriting

Thomas Traversié, Florian Rabe

Representation theorems for formal systems often take the form of an inductive translation that satisfies certain invariants, which are proved inductively. Theory morphisms and log…