Re-factored both semantics to include the modifications to call (in to out) and return (out to in).
This should be pushed in a separate branch, if i did all correctly.
Full abstraction for the new corrected semantics, proven!
Defined contextual equivalence.
Correct usage of returnback entry point via the stack.
Formalised trace equivalence.
Factored out the labels into a separate file.
Merge commit 'f91d59092d6b71fcd8e5c63ae79e5255e9bbe5d9' into extraCallRet