I will demonstrate the Coq formalization of Iris – a framework for higher-order concurrent separation logic. A novel feature of the Coq formalization of Iris is its support for interactive proofs in the logic. We have achieved that by extending Coq with spatial and non-spatial named contexts for the hypotheses of Iris. Using these contexts we have implemented Coq-like tactics for reasoning in the Iris logic. In this talk, I will discuss the Coq implementation of Iris and demonstrate how it can be used for verification of sequential and concurrent programs.