Abstract compilation is a novel approach to static type analysis aiming to reconcile types, symbolic execution and compiler technology: analyzing an expression consists in solving the goal generated from its compilation w.r.t. the coinductive model of the constraint logic program generated from the compilation of the source program where the expression is executed. In such a model terms are types representing possibly infinite sets of values, and goal resolution corresponds to symbolic execution. Abstract compilation is particularly suited for defining and implementing type inference and global type analysis of object-oriented languages modularly: indeed, it is possible to provide several compilation schemes for the same language, each corresponding to a different kind of analysis, without changing the inference engine, which implements coinductive constraint logic programming (where constraints are expressed through a suitable subtyping relation).

In this talk I will present some examples of use of abstract compilation, and discuss some challenging issues concerning proofs of soundness and completeness of subtyping between coinductive types, and, more in general, proofs of soundness of abstract compilation schemes.