Incremental and parallel checking of dependently typed programs
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. Current languages with support for dependent types such as Agda often suffer from slow type checking, which results in unresponsive editor services as these often depend on the result of type checking. The goal of this project is to investigate the extend to which a type checker for dependent types can be made fully incremental and parallel, so that it can be used for interactive editing of code.

Further reading

• Taico Aerts: Incrementalizing Statix: A Modular and Incremental Approach for Type Checking and Name Binding using Scope Graphs (2019)
• Aron Zwaan: Incremental type-checking for free: using scope graphs to derive incremental type-checkers (2022)
• Peter Fogg, Sam Tobin-Hochstadt, Ryan R. Newton: Parallel type-checking with haskell using saturating LVars and stream generators (2016)

Contacts for the project

• Jesper Cockx (TU Delft)
• Bohdan Liesnikov (TU Delft)