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

Abstract

Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, well-typed implementation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by providing a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators. We only allow case splits on variables from a fixed universe of data type descriptions, for which we use techniques like basic analysis and specialization by unification.

Thesis

https://repository.tudelft.nl/record/uuid:e91ef1ea-942e-4f11-a1c4-bb82f444aaed