A generic translation from case trees to eliminators
Master Project of Kayleigh Lieverse

Project description

In dependent type theory, each inductive datatype comes with a datatype eliminator that expresses the induction principle for that datatype and can be used to define functions on it. While powerful, eliminators are not very user-friendly and hence many high-level dependently typed languages provide more convenient syntax in the form of dependent pattern matching. To minimize the trusted base of a language, it is desirable to translate these definitions back to eliminators. This translation is done in two steps: first the clauses of the definition are translated to a case tree and then this case tree is subsequently translated to the eliminators. The first step is specific to each language, but the second step could be done generically. The goal of this project would be to give a generic implementation of this translation, which would greatly decrease the burden of implementing the overall translation.

Contacts for the project

• Lucas Escot (TU Delft)
• Jesper Cockx (TU Delft)