Executable Denotational Semantics With Interaction Trees