diff --git a/thesis.tex b/thesis.tex index 41af760..3ea33a7 100644 --- a/thesis.tex +++ b/thesis.tex @@ -698,10 +698,9 @@ callcc, J, catchcont, etc. \paragraph{Landin's J operator} % \begin{reductions} - \slab{Marking} & \EC[(\lambda x.M)~V] &\reducesto& \EC[\lambda^{\EC}.M[V/x]], \text{where $\EC$ contains no other $\lambda$}\\ - \slab{Return} & \lambda^{\EC}.V &\reducesto& V\\ - \slab{Capture} & \lambda^{\EC}.\EC'[\J\,x.M] &\reducesto& \EC'[\cont_{\Record{\EC;x.M}}/k]\\ - \slab{Resume} & \EC[\Continue~\cont_{\Record{\EC';x.M}}~V] &\reducesto& \EC'[M[V/x]] + \slab{Dump} & \EC[(\lambda x.M)~V] &\reducesto& \EC[\mathcal{D}[M[V/x]]]\\ + \slab{Capture} & \EC[\mathcal{D}[\J\,(\lambda x.M)]] &\reducesto& \EC[\mathcal{D}[\cont_{\Record{\EC;\lambda x.M}}]]\\ + \slab{Resume} & \EC[\Continue~\cont_{\Record{\EC';\lambda x.M}}~V] &\reducesto& \EC'[(\lambda x.M)~V] \end{reductions} %