364 Hoang, Thai Son Proof of correctness for interface instantiation. [Rodin Archive]