Relational Solver for Java Generics Type System

In this talk, we will describe a solver for Java generics type system that was implemented using relational verifier-to-solver approach. The solver finds solutions for a system of subtyping inequations with free variables, and thus can be used to determine a concrete type satisfying a set of constraints. Also, we will discuss the relational verifier-to-solver approach, some extra-relational optimizations we used in the implementation and possible applications of the solver.
(Joint work with Dmitry Kosarev, Dmitry Ivanov and Dmitry Boulytchev.)