SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 13:20 - 13:40 at SPLASH-I - T-4 Chair(s): Michael Pradel, Sophia Drossopoulou
Wed 18 Nov 2020 01:20 - 01:40 at SPLASH-I - T-4 Chair(s): Sophia Drossopoulou, Julien Lange

Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type systems. In this paper, we propose a systematic approach for deriving incremental type checkers from textbook-style type system specifications. Our approach is based on compiling inference rules to Datalog, a carefully limited logic programming language for which incremental solvers exist. The key contribution of this paper is to discover an encoding of the infinite typing relation as a finite Datalog relation in a way that yields efficient incremental updates. We implemented the compiler as part of a type system DSL and show that it supports simple types, some local type inference, operator overloading, universal types, and iso-recursive types.

Tue 17 Nov

Displayed time zone: Central Time (US & Canada) change

Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change