Dependent Types and Conversion Checking

Dependent Types and Conversion Checking: A literature survey on implementation techniques for type systems

Khakimova, Maria (TU Delft Electrical Engineering, Mathematics and Computer Science)

Cockx, J.G.H. (mentor)
Liesnikov, B. (mentor)
Panichella, Annibale (graduation committee)

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2023-06-28

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 - \nameref{naive}, \nameref{NbE}, \nameref{generalShape}, \nameref{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.

Dependent Types
Conversion Checking
Type Checking
Definitional Equality
Type Systems

http://resolver.tudelft.nl/uuid:e9e1952f-e977-4632-a5f5-1ab16baf4350

Student theses

bachelor thesis

© 2023 Maria Khakimova