A variant of typed \(\lambda\)-calculus that makes evaluation order explicit.
This helps with capturing effects formally. "functional/imperative synthesis" (Levy)
Types come in two polarities:
\[ \begin{array}{lll} B^- &::= & A^+ \rightarrow B^-\ |\ \uparrow{A^+} \\ A^+ &::= &\mathbf{1}\ |\ \downarrow{B^-} \end{array} \]