We present a formalization of logical refinements of programs in a higher-order programming languages with general references, polymorphism and existential types, and concurrency. The logical refinement is sound w.r.t. contextual refinements of programs, and has been formalized in Coq, together with a number of case studies, in state of the art concurrent separation logic Iris. The work extends on the initial interpretation of logical relations in Iris by Krebbers et al., to the extent that we provide a calculus that allows one to reason about logical refinement in an abstract way, together with a collection of Coq tactics that make reasoning in the calculus tractable for realistic examples.