PRL Seminars 1998-99

I will finish my presentation of our latest work. I will concentrate on the type checking algorithm. This is joint work with Christoph Kreitz.

We present a system for automatic debugging in typed functional languages. The system checks program properties specified by a user and finds bugs as well as conditions necessary to avoid them. It applies type-checking techniques built on top of the existing type system of the programming language. Its type system is based on the notion of set types, extended through type constructors, polymorphism and dependent types. Subtyping is used to allow finer specification. Type checking is achieved by collecting flow information through flow types and constraints on them. By solving the constraints we obtain instances for flow type variables and a set of conditions that make the typing provable. These conditions are converted into arithmetical formulae that can be checked by a common decision procedure. Our approach has a modular structure and can also be used for array bounds checking and other program analysis problems.