Thursday 19 September 2019, 14:00, LSV library: Importing Agda proofs in Logipedia, Guillaume Genestier (PhD student, Deducteam).

In this talk, I will present the work performed in collaboration with Jesper Cockx and Andreas Abel during my stay in Chalmers University this summer. The goal was to implement a translator between Agda and Dedukti. On practical aspects, I will present the translator I implemented and the fragment of the standard library I was able to translate. On the theoretical aspects, the main results obtained are an encoding of universe polymorphism without cumulativity (a hot topic in the team today, as you may know) and the eta-conversion (especially for record types).