This talk will describe “interaction trees,” a Coq datatype for describing the behaviors of systems that interact with their environments. Several DeepSpec projects have found a use for this data structure and accompanying theory. This talk will highlight its use for defining memory models as part of the ongoing Vellvm efforts to define semantics of the LLVM IR.