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.
Further reading
- Thierry Coquand: An algorithm for testing conversion in type theory (1991)
- Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey: Better Together: Unifying Datalog and Equality Saturation
- Kontroli-rs, a fast and parallel implementation of a dependently typed language in Rust
Contacts for the project
- Jesper Cockx (TU Delft)
- Bohdan Liesnikov (TU Delft)
Supervisor(s): Jesper Cockx
Posted: June 02, 2023