The authors would like to thank Robert Harper for pointing out the connection between evaltrace notation and Plotkin's structured operational semantics.