| $$\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}$$
+| $$\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 | +