IPA Fall days 2017 – Type-based static analysis

By Jurriaan Hage

As the halting problem in general is undecidable, it is possible that some programs can have a correct execution, but are not type-correct. That is why we need to study accuracy. To be on the safe side: the above example is considered wrong (in their setting), and you need to advance the type system to add that program. It turns out there is a tension between accuracy and modularity: whole program analysis typically yields better results. So, how do you type-check a language?  A lot of fun with SOS rules 🙂 and algorithms to come up with valuations..