Dependent Types and Conversion Checking

A literature survey on implementation techniques for type systems

Bachelor thesis (2023)

Authors

M. Khakimova Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (supervisor 1)
B. Liesnikov Programming Languages - EEMCS (supervisor 1)
Annibale Panichella (supervisor 2)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Maria Khakimova
Type Checking Dependent Types Conversion Checking Definitional Equality Type Systems
More Info
expand_more

Published Date

28-06-2023

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

While dependent types can allow programmers to verify properties of their programs, implementing a type checker for a dependent type theory is often difficult. This is due to the fact that, in the presence of dependent types, deciding the equality of types - conversion checking - becomes non-trivial. Due to an identified gap in literature regarding a survey of existing techniques for implementing conversion checking in the presence of dependent types, this paper aims to provide an exploratory overview of the current state of this field.

We identify five distinct implementation strategies within this paper. Four of these techniques were different from a theoretical standpoint -
ameref{naive},
ameref{NbE},
ameref{generalShape},
ameref{hersub}, and a technique using congruence closure. They all have different benefits and drawbacks regarding their portability, extendability to richer type systems, efficiency, and decidability. Additionally, three techniques that focused on improving the efficiency of conversion checking through the use of an abstract machine or compilation into native code were found.