A Generic Translation from Case Trees to Eliminators

A Generic Translation from Case Trees to Eliminators

Lieverse, Kayleigh (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Cockx, J.G.H. (mentor)
Escot, L.F.B. (graduation committee)
Kulahcioglu Ozkan, Burcu (graduation committee)

Delft University of Technology

Computer Science

2024-06-20

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.

Dependent Types
Pattern matching
Elimination
Elaboration

http://resolver.tudelft.nl/uuid:e91ef1ea-942e-4f11-a1c4-bb82f444aaed

https://github.com/klieverse/case-trees-to-eliminators Formalization of this thesis in Agda.

Student theses

master thesis

© 2024 Kayleigh Lieverse