Incremental Type Checking in IncA

Incremental Type Checking in IncA

Bosma, Sander (TU Delft Electrical Engineering, Mathematics and Computer Science)

Erdweg, Sebastian (mentor)
Szabo, Tamas (mentor)
Visser, Eelco (graduation committee)
Katsifodimos, Asterios (graduation committee)
Krebbers, Robbert (graduation committee)

Delft University of Technology

Computer Science

2018-11-02

When using an integrated development environment, it is desirable to get real-time feedback on the correctness of the program. That is, we want to see the results of the type checker in real-time. However, type checking can take a long time, especially when the subject program is large. To be able to provide real-time results, we need to incrementalize the type checker. This way, when a program changes, we only need to recalculate results for the changed portion of the program, and everything that depends on it. In this thesis, we discuss how we used IncA to implement a type checker for Rust. IncA is a domain specific language for the definition of incremental program analyses: analyses written in IncA are automatically incrementalized. We show in our evaluation that our type checker updates results significantly faster than its non-incremental counterpart. While we were able to successfully implement many of Rust's features, there are some parts we were unable to implement, and we show why that is the case.

type checking
incremental
Static Analysis

http://resolver.tudelft.nl/uuid:95fd2998-1b39-4dd1-aba4-b2f73b443828

Student theses

master thesis

© 2018 Sander Bosma