Composable Soundness Proofs for Static Analysis using Arrows

For the next Meetup, Sven Keidel will give a talk about how he uses Haskell in his PhD work to solve problems in the area of static analysis.

As usual, we will start at 18:30 with Pizza and afterwards start with the talk.

Here is the full abstract:

Static analyzers are tools that calculate information about the execution of programs without actually running the programs. For example, a type checker is a static analysis that calculates the shape of values a program can evaluate to. One important property of static analyses is that they are sound, in other words, that the static information correctly predicts the execution of a program. For example, a sound type checker guarantees that type-correct programs do not crash due to a type mismatch.
However, proving that a static analysis is sound is challenging because of the high proof complexity and proof effort.

In this talk I will explain how static analyses can be structured with Haskell arrows to decompose their soundness proof into smaller soundness lemmas that are easier to prove. Even though this talk is based on a ICFP paper (https://dl.acm.org/citation.cfm?id=3236767­), I will make the talk self-contained and require no knowledge about static analysis.