An evaluation of algorithms for conversion checking

An evaluation of algorithms for conversion checking
Master Project

Problem statement

Dependent type systems can help writing programs that satisfy their intended specifications by embedding these specifications in the types of the programs. However, dependent type systems are currently restricted to relatively niche languages such as Coq and Agda. One hindrance to their adoption is the performance cost their incur during type checking: a dependent type checker must be able to compare arbitrary terms for equality. The part of the type checker that is responsible for this comparison is called the conversion checker, and there have been different techniques proposed in the literature. But since these techniques are not implemented for the same language, it is difficult to compare them directly.

Project description

The goal of this project is to provide a thourough comparison of different techniques for checking conversion of terms in dependently typed languages. In particular, the following techniques exist in the literature:

Naive substitution-based reduction combined with a comparison of the weak-head normal forms
Using an abstract machine for reduction combined with a comparison of the weak-head normal forms
Using an abstract machine for both reduction and comparison of terms
Approximate conversion checking
Compilation of terms to native code
Using bottom-up equality saturation algorithms such as Egg
Using logic programming and database techniques such as Datalog

The goal of this project is to implement a type checker for a small dependently typed lambda calculus which can be configured to use most or all of these techniques for conversion checking, and to construct a benchmark of different test cases that can be used to evaluate the performance characteristics of these techniques.