An execution trace \(t\)  of a program \(p\)  is a path in \({p}\)  starting
from the beginning vertex \({p}\) . It can be checked that those are in
bijection with execution traces as they would be defined in a reasonable
operational semantics [1]}. Moreover, \(n\) -cubes of dimension 2 and
higher can be used to construct a useful notion of equivalence of execution
traces, called homotopy, as explained in Section .
