

\clearpage{}
% -------------------------------------------------------------------
\subsection{Material functions and constants}
In this paper we work at an abstraction level where the only objects kept in the mutable store have type @Ref@. Objects of type @Unit@, @Bool@ and @Nat@ are treated as primitive pure values, are not updatable, and for a concrete implementation we assume they would be held in registers rather than in main memory.

Similarly, we also treat functions and type abstractions as pure values. The introduction forms $(\lambda \bra{z} : type.~ exp)$ and $(\Lambda \bra{a} : kind.~ exp)$ to not include region variables, and we substitute these values freely into other values and expressions. The semantics we give does not specify where functional values would be stored in a concrete implementation, or how to represent the result of a substitution. Real functional language implementations such as \CITE handle this by lambda lifting the intermediate code to supercombinators, and then building partial application (PAP) objects at runtime that contain code pointers to these supercombinators. Our presentation is intentionally more abstract, and we do not formalize these operational details.

In contrast, languages such as in \cite{Helsen:soundness-region-calclus} are more operational in nature, placing all values in regions (including functions), though like us their dynamic semantics uses substitution to perform function application. Programs in these languages can be represented in our system by a simple type directed desugaring. A lambda abstraction in \cite{Helsen:soundness-region-calclus} would be written $(\lambda z : t.~ x) ~\tt{at}~ r$, where $r$ states the region in which to allocate the function closure. We would desugar this to our system using the following rule, that wraps a pure function abstraction in a heap allocated closure object. 
$$
\ruleIL {DsLam}
{       \KindT  {\mke}{\msp}{t_1}{\kcData}
        \qq
        \TypeX  {\mke}
                {\mte,~ \bra{z} : t_1}
                {\mse}
                {\msp}
                {x_2}
                {t_2}
                {\bot}
}
{ \begin{array}{ll}
        \mke ~|~ \mte ~|~ \mse ~|~ \msp 
        & \vdash  \cx{(\lambda \bra{z} : t_1.~ x_2)~ \tt{at}~ r_1}
                  ~ \stackrel{\mbox{\tiny def}}{=} ~
                  \cx{\tt{alloc}~ r_1~ (\lambda \bra{z} : t_1.~ x_2)}\\
        &  ::  ~~ \ct{\tt{Closure}~ r_1~ (\tto{t_1}{e_1}{t_2})}
           ~~; ~~ \ct{\tcAlloc~ r_1}
  \end{array}
}
$$

Here, @Closure@ is a synonym for @Ref@, but we use a different name to highlight that objects of type @Closure@ are only constructed via this rule. Applications of closures are then desugared by reading the functional value from the closure before using our pure application form.
$$
\ruleIL {DsApp}
{       \TypeV  {\mke}{\mte}{\mse}{\msp}
                {v_1}
                {\tt{Closure}~ r_1~ (\tto{t_1}{e_1}{t_2})}
        \qq
        \TypeV  {\mke}{\mte}{\mse}{\msp}
                {v_2}
                {t_1}
}
{ \begin{array}{ll}
        \mke ~|~ \mte ~|~ \mse ~|~ \msp  
        & \hspace{-1ex}
          \vdash \cx{\tt{app}~ v_1~ v_2}  
                  ~ \stackrel{\mbox{\tiny def}}{=} ~
                 \cx{(\klet~ f = \kread~ r_1~ v_1~ \kin~ f~ v_2)} \\
        & \hspace{-1ex}
          :: ~~ \ct{t_2} ~~;~~ \ct{\tcRead~ r_1 \vee r_1}
  \end{array}
}
$$

Note that both the construction and application of a closure now performs an effect, which mirrors the system of \cite{Helsen:soundness-region-calclus}. 


\clearpage{}
