Interaction treees are coinductive structures, which can particularly be used to model operational semantics. They can be verified, using coinduction techniques, and are also inherently executable, which makes them ideal for simulations and verified implementations. An interaction tree models three kinds of behaviour: (1) terminating, with a return value of type 'r; (2) an internal silent step (τ); or (3) a choice between several visible events drawn from type 'e. We use interaction trees extensively in Isabelle/UTP to enable coinductive reasoning, and animation of formal models. For more information, please see our CONCUR 2021 paper.