Encoding Agda Programs Using Rewriting
Guillaume Genestier · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2020
We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.