Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification