Semantics of Partial Programs

Formally speaking, for most programming languages, only complete programs have a well-defined semantics. Many tools in a language's ecosystem, particularly IDEs, however, also work on partial programs in order to help programmers to eventually write a complete one. As such, an IDE has to guess the plausible complete programs based on whatever a programmer has written so far. This is typically based on lots of heuristics and special cases, which is one of the reasons why full-fledged IDE functionality is limited to relatively few languages.

The goal of this project is to look heuristically at the problem of IDEs, starting with the design of language's syntax and type system, and come up with formal properties of good language definitions and parsing and type-checking algorithms that work well with each other to provide good IDE support in a principled way.