| $$\begin{aligned} - \tau_p ::= &\; R\ &[real] \\ - \ | &\; N\ &[nat] \\ - \tau ::= &\; \tau_p\ & \\ - \ | &\; \tau \to \tau \ &[function] \\ - % |&\quad \langle \tau \rangle - \end{aligned}$$ Types | -$$\begin{aligned} - v_p \; ::=& \ r \quad r \in \mathbb{R} \\ - |& \ n \quad n \in \mathbb{N}\\ - v \; ::=&\ v_p \\ - |& \ cls(\lambda\ x.e, E) \\ - %%|& \quad (e_1,e_2) \quad & [product]\\ - %%|& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\ - %%|& \quad \langle e \rangle \quad & [code] \\ - %%|& \quad \textasciitilde e \quad & [escape] - \end{aligned}$$ Values | -
| $$\begin{aligned} -e \; ::=& \ x &x \in {v_p} \ & [value]\\ - |& \ \lambda x.e & & [lambda]\\ - |& \ let\; x = e_1\; in\; e_2 & & [let]\\ - |& \ fix \; x.e & & [fixpoint]\\ - |& \ e_1 \; e_2 & & [app]\\ - |& \ if\; (e_c)\; e_t\; else\; e_e \; & & [if] \\ - |& \ delay\; n \; e_1 \; e_2 &n \in \mathbb{N}\ & [delay]\\ - |& \ feed \; x.e & & [feed]\\ - |& ... & & \\ - %%|& \quad (e_1,e_2) \quad & [product]\\ - %%|& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\ - %%|& \quad \langle e \rangle \quad & [code] \\ - %%|& \quad \textasciitilde e \quad & [escape] - \end{aligned}$$ Terms | -|
$$\centering - \begin{aligned} - let\ & onepole = \\ - & \ \lambda x. \lambda g.\ feed\ y.\ x *(1.0 - g) + y * g \ in\ ... - \end{aligned}$$
+$$ +\begin{aligned} + let\ & onepole = \\ + & \ \lambda x. \lambda g.\ feed\ y.\ x *(1.0 - g) + y * g \ in\ ... +\end{aligned} +$$| $$\frac{\Gamma, x:\tau_a \vdash e:\tau_b}{\Gamma \vdash \lambda x.e:\tau_a \to \tau_b }$$T-LAMBDA | -$$\frac{ \Gamma \vdash e_1:N \quad \Gamma \vdash e_2:\tau }{\Gamma \vdash delay\ e_1\ e_2 : \tau}$$T-DELAY | -
| $$\frac{\Gamma, x : \tau_p \vdash e: \tau_p }{\Gamma \vdash feed\ x.e:\tau_p}$$T-FEED | -$$\frac{ \Gamma \vdash e_c : R\ \Gamma \vdash e_t:\tau\ \Gamma \vdash e_e:\tau }{\Gamma \vdash if\ (e_c)\ e_t\ e_e\ : \tau}$$T-IF | -