  We present guarded interaction trees -- a structure and a fully formalized
framework for representing higher-order computations with higher-order effects
in Coq, inspired by domain theory and the recently proposed interaction trees.
We also present an accompanying separation logic for reasoning about guarded
interaction trees. To demonstrate that guarded interaction trees provide a
convenient domain for interpreting higher-order languages with effects, we
define an interpretation of a PCF-like language with effects and show that this
interpretation is sound and computationally adequate; we prove the latter using
a logical relation defined using the separation logic. Guarded interaction
trees also allow us to combine different effects and reason about them
modularly. To illustrate this point, we give a modular proof of type soundness
of cross-language interactions for safe interoperability of different
higher-order languages with different effects. All results in the paper are
formalized in Coq using the Iris logic over guarded type theory.
