In this talk, we will discuss the current results and ongoing works on proving the type soundness of a merge system via semantic typing.