to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H\cup\\{l\mapsto_{t}\lambda_{t}({x:\square}).{m}\\};{*l}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
38.20876pt\vbox{\hbox{\hskip-38.20874pt\hbox{\hbox{$\displaystyle\displaystyle
H;m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};m^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
48.11087pt\vbox{\vbox{}\hbox{\hskip-48.11086pt\hbox{\hbox{$\displaystyle\displaystyle
H;m\ n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};m^{\prime}\
n$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
35.70876pt\vbox{\hbox{\hskip-35.70874pt\hbox{\hbox{$\displaystyle\displaystyle
H;n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};n^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
48.11087pt\vbox{\vbox{}\hbox{\hskip-48.11086pt\hbox{\hbox{$\displaystyle\displaystyle
H;m\ n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};m\
n^{\prime}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
55.14474pt\vbox{\hbox{\hskip-55.14473pt\hbox{\hbox{$\displaystyle\displaystyle\textit{lookup}({H},{l},{\lambda_{t}\\{{x:\square}\\}.{m}},{H^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
55.2689pt\vbox{\vbox{}\hbox{\hskip-55.2689pt\hbox{\hbox{$\displaystyle\displaystyle
H;{*l}\ n\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};m[\square/x]$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
54.90472pt\vbox{\hbox{\hskip-54.90472pt\hbox{\hbox{$\displaystyle\displaystyle\textit{lookup}({H},{l_{1}},{\lambda_{t}({x:\square}).{m}},{H^{\prime}})$}}}\vbox{}}}\over\hbox{\hskip
54.41113pt\vbox{\vbox{}\hbox{\hskip-54.41113pt\hbox{\hbox{$\displaystyle\displaystyle
H;{*l_{1}}\
{*l_{2}}\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\displaystyle\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\displaystyle\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}m[{*l_{2}}/x]$}}}}}}$
Figure 20. Heap Reductions

Generally for redexes in the heap semantics, pointers are expected in place of
values in the standard program semantics. For example, the application of two
pointers ${*l_{1}}\ {*l_{2}}$ is considered a $\beta_{1}$-redex if ${*l_{1}}$
points to a relevant $\lambda{1}$-program in the heap. To reduce this redex,
the argument pointer ${*l_{2}}$ is substituted into the body of the
$\lambda{1}$-program referenced by ${*l_{1}}$. Likewise, the application form
${*l}\ n$ is considered a $\beta_{0}$-redex if ${*l}$ points to an irrelevant
$\lambda{0}$-program in the heap. For extracted programs satisfying the
erasure relation, the argument $n$ here must be $\square$ so we immediately
substitute $\square$ into the body of the $\lambda{0}$-program referenced by
${*l}$.

###  8.3. Pointer Resolution

We do not extend our typing rules or standard operational semantics to cover
pointer expressions, so whenever there is ${\Gamma;\Delta\vdash m:A}$ or
${m\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}n}$ we know that
all terms involved must not contain pointers. Instead, we introduce a new
judgment ${H;m\sim n}$ presented in Figure 21 which recursively dereferences
all pointers in $m$ using heap $H$ until there are no pointers occurring in
$n$.

$\displaystyle\displaystyle{\hbox{\hskip
10.73126pt\vbox{\hbox{\hskip-10.73125pt\hbox{\hbox{$\displaystyle\displaystyle
H\triangleright\text{U}$}}}\vbox{}}}\over\hbox{\hskip
17.25pt\vbox{\vbox{}\hbox{\hskip-17.25pt\hbox{\hbox{$\displaystyle\displaystyle
H;x\sim x$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
38.43262pt\vbox{\hbox{\hskip-38.43262pt\hbox{\hbox{$\displaystyle\displaystyle
H\triangleright t$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
H;m^{\prime}\sim m$}}}}\vbox{}}}\over\hbox{\hskip
58.66518pt\vbox{\vbox{}\hbox{\hskip-58.66518pt\hbox{\hbox{$\displaystyle\displaystyle
H;\lambda_{t}\\{{x:\square}\\}.{m^{\prime}}\sim\lambda_{t}\\{{x:\square}\\}.{m}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
38.43262pt\vbox{\hbox{\hskip-38.43262pt\hbox{\hbox{$\displaystyle\displaystyle
H\triangleright t$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
H;m^{\prime}\sim m$}}}}\vbox{}}}\over\hbox{\hskip
55.66515pt\vbox{\vbox{}\hbox{\hskip-55.66515pt\hbox{\hbox{$\displaystyle\displaystyle
H;\lambda_{t}({x:\square}).{m^{\prime}}\sim\lambda_{t}({x:\square}).{m}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
19.45135pt\vbox{\hbox{\hskip-19.45135pt\hbox{\hbox{$\displaystyle\displaystyle
H;m^{\prime}\sim m$}}}\vbox{}}}\over\hbox{\hskip
32.20137pt\vbox{\vbox{}\hbox{\hskip-32.20137pt\hbox{\hbox{$\displaystyle\displaystyle
H;m^{\prime}\ \square\sim m\ \square$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
47.92273pt\vbox{\hbox{\hskip-47.92273pt\hbox{\hbox{$\displaystyle\displaystyle
H_{1};m^{\prime}\sim m$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle H_{2};n^{\prime}\sim
n$}}}}\vbox{}}}\over\hbox{\hskip
40.92271pt\vbox{\vbox{}\hbox{\hskip-40.92271pt\hbox{\hbox{$\displaystyle\displaystyle
H_{1}\mathbin{\mathaccent 0{\cdot}\cup}H_{2};m^{\prime}\ n^{\prime}\sim m\
n$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
59.80013pt\vbox{\hbox{\hskip-59.80013pt\hbox{\hbox{$\displaystyle\displaystyle\textit{lookup}({H},{l},{v^{\prime}},{H^{\prime}})$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle H^{\prime};v^{\prime}\sim
v$}}}}\vbox{}}}\over\hbox{\hskip
17.13022pt\vbox{\vbox{}\hbox{\hskip-17.1302pt\hbox{\hbox{$\displaystyle\displaystyle
H;{*l}\sim v$}}}}}}$ Figure 21. Pointer Resolution

When defining the judgment ${H;m\sim n}$, care is taken to ensure that
dereferencing pointers obey the no-weakening and no-contraction principles
analogously to the program typing rules. In other words, pointers to linear
mappings in $H$ are dereferenced only once. This is accomplished by enforcing
side conditions ${H_{1}\mathbin{\mathaccent 0{\cdot}\cup}H_{2}}$ and
$H\triangleright s$ which basically perform the same roles as their typing
counterparts. The only rule without a typing counterpart is the last rule
where it initially dereferences pointer ${*l}$ to value $v^{\prime}$ and
recursively resolves all pointers in $v^{\prime}$ using the remaining heap
$H^{\prime}$.

To reintroduce typing information back into programs containing pointer
expressions, we develop the ternary relation of well-resolved programs
presented in Figure 22 that unites the erasure relation of Section 5 and
pointer resolution. For a valid instance of well-resolved ${H\vdash a\sim
b\sim c:A}$ we know that $a$ is a well-type program that extracts to $b$ and
resolving the pointers in $c$ also gives us $b$. Essentially, the extracted
program $b$ serves to bridge the well-typed original program $a$ and the
pointer program $c$.

$\displaystyle\displaystyle{\hbox{\hskip
53.32295pt\vbox{\hbox{\hskip-53.32294pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon;\epsilon\vdash
a\sim b:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle H;c\sim
b$}}}}\vbox{}}}\over\hbox{\hskip
34.73857pt\vbox{\vbox{}\hbox{\hskip-34.73856pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash a\sim b\sim c:A$}}}}}}$ Figure 22. Well-Resolved

From the definition of pointer resolution it is clear that the contents in
heap $H$ greatly influence the outcome of resolving pointer program $m$ in
judgment ${H;m\sim n}$. To characterize the heaps produced during heap
reduction, we introduce in Figure 23 a judgment $H~{}\textit{wr-heap}$ stating
that $H$ is of a form that could plausibly be produced by heap reduction.
Basically, all locations in $H$ map to closed values. This means that
performing lookup in heaps satisfying the wr-heap property is guaranteed to be
productive because a value is retrieved after one level of indirection. The
wr-heap property serves as an inductive invariant in the proof of heap
semantics soundness, informing us of the structure of heaps at every reduction
step.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.08757pt\vbox{\vbox{}\hbox{\hskip-19.08755pt\hbox{\hbox{$\displaystyle\displaystyle\epsilon~{}\textit{wr-
heap}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
82.36525pt\vbox{\hbox{\hskip-82.36525pt\hbox{\hbox{$\displaystyle\displaystyle\textit{FV}({m})/\\{x\\}=\emptyset$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle H~{}\textit{wr-heap}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle l\notin
H$}}}}}\vbox{}}}\over\hbox{\hskip
57.5165pt\vbox{\vbox{}\hbox{\hskip-57.5165pt\hbox{\hbox{$\displaystyle\displaystyle
H\cup\\{l\mapsto_{t}\lambda_{t}\\{{x:\square}\\}.{m}\\}~{}\textit{wr-
heap}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
82.36525pt\vbox{\hbox{\hskip-82.36525pt\hbox{\hbox{$\displaystyle\displaystyle\textit{FV}({m})/\\{x\\}=\emptyset$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle H~{}\textit{wr-heap}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle l\notin
H$}}}}}\vbox{}}}\over\hbox{\hskip
56.01648pt\vbox{\vbox{}\hbox{\hskip-56.01648pt\hbox{\hbox{$\displaystyle\displaystyle
H\cup\\{l\mapsto_{t}\lambda_{t}({x:\square}).{m}\\}~{}\textit{wr-heap}$}}}}}}$
Figure 23. WR-Heaps

###  8.4. Soundness of Heap Semantics

The soundness of heap semantics is again justified through progress-
preservation style theorems. Due to the fact that these theorems must now
account for program typing, erasure, pointer resolution, heap reductions and
many other concepts simultaneously, their statements and proofs become
significantly more involved than previous versions.

The first theorem that we present is resolution stability. It is reminiscent
of the value stability theorem (Theorem 11). But instead of exploring the
constraints set by the modality of values on their program contexts as in the
value stability case, the resolution stability theorem derives constraints on
the mappings inside heaps.

###### Theorem 1 (Resolution Stability).

Given valid instances of well-resolved ${H\vdash a\sim b\sim c:A}$, logical
typing ${\epsilon\vdash A:s}$ and ${H~{}\textit{wr-heap}}$, if $b$ is a value
then heap $H$ can be upper bound by constraint ${H\triangleright s}$.

The heap subject reduction theorem propagates the well-resolved and wr-heap
invariants across heap reduction, ensuring that pointer programs well-resolved
in wr-heaps always reduce to programs that are well-resolved in wr-heaps.
Additionally, heap reductions agree with iterated steps in the standard
semantics for original programs and extracted programs.

###### Theorem 2 (Heap Subject Reduction).

Given instances of well-resolved ${H\vdash a\sim b\sim c:A}$ and
${H~{}\textit{wr-heap}}$, then for heap reduction
${H;c\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};c^{\prime}}$
there exist $a^{\prime}$ and $b^{\prime}$ such that the following judgments
${H^{\prime}\vdash a^{\prime}\sim b^{\prime}\sim c^{\prime}:A}$,
${H^{\prime}~{}\textit{wr-heap}}$,
${a\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}^{*}a^{\prime}}$
and ${b\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}^{*}b^{\prime}}$
all hold.

Finally, the heap progress theorem shows that for any pointer program $c$ that
is well-resolved in a heap $H$ satisfying the wr-heap condition, either there
exists a heap reduction
${H;c\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};c^{\prime}}$
or $c$ is a pointer. From the definition of wr-heap we know that all elements
contained in the heap are values. In the case that $c$ is a pointer,
dereferencing $c$ yields a value.

###### Theorem 3 (Heap Progress).

Given valid instances of well-resolved ${H\vdash a\sim b\sim c:A}$ and
${H~{}\textit{wr-heap}}$, then either there exist heap $H^{\prime}$ and
program $c^{\prime}$ such that there is reduction
${H;c\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H^{\prime};c^{\prime}}$
or there exists a location $l$ such that ${c={*l}}$.

Starting from a well-typed closed program $m$ and an empty heap, due to the
fact that empty heaps are degenerate wr-heaps and well-typed closed programs
are trivially well-resolved in empty heaps, the heap subject reduction theorem
and heap progress theorem allow for heap reductions to be repeatedly generated
and applied until a value referencing pointer is reached. The resolution
stability theorem tells us that the heap at this point can be constrained by
${H\triangleright s}$ where $s$ is the sort of the original program $m$’s
type. In practice, if the designated starting main expression is required to
be of a non-linear type, all allocated heap memory will be safely freed by the
time that the program terminates.

##  9\. Extensions

In this section, we describe some useful extensions to the core TLL language
for program development and reasoning. The meta theoretic results presented in
the previous sections can all be extended naturally to cover these additions.
In fact, our theorems are all proven assuming the inclusion of these
extensions.

###  9.1. Propositional Equality

The first extension that we present is propositional equality with logical
typing rules given in Figure 24. This is the usual propositional equality
found in intensional dependent type theories which allows one to posit
equality between two terms. Equality and its proofs exist purely for reasoning
purposes so they can only be derived at the logical level. However, a proof of
equality constructed at the logical level can be eliminated at the program
level using the rule shown in Figure 25. This allows the type-casting of
programs with a proof that the target type is propositionally equal to the
original type. A simple example of program level equality elimination in
practice is the type-casting of a length indexed vector ls with type
$\textit{vec}\ (x+y)\ A$ to type $\textit{vec}\ (y+x)\ A$ by appealing to the
proof that addition is commutative.

$\displaystyle\displaystyle{\hbox{\hskip
72.32407pt\vbox{\hbox{\hskip-72.32407pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
A:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:A$}}}}}\vbox{}}}\over\hbox{\hskip
23.47964pt\vbox{\vbox{}\hbox{\hskip-23.47963pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash{m}=_{A}{n}:\text{U}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
19.13858pt\vbox{\hbox{\hskip-19.13857pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:A$}}}\vbox{}}}\over\hbox{\hskip
32.9432pt\vbox{\vbox{}\hbox{\hskip-32.94319pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash{\text{refl}\;{m}}:{m}=_{A}{m}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
141.48695pt\vbox{\hbox{\hskip-141.48695pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,p:{m}=_{A}{x}\vdash
B:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
H:B[m/x,{\text{refl}\;{m}}/p]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
P:{m}=_{A}{n}$}}}}}\vbox{}}}\over\hbox{\hskip
60.53145pt\vbox{\vbox{}\hbox{\hskip-60.53145pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\text{R}_{[x,p]B}^{=}({H},{P}):B[n/x,P/p]$}}}}}}$
Figure 24. Propositional Equality (Logical Rules)
$\displaystyle\displaystyle{\hbox{\hskip
147.23697pt\vbox{\hbox{\hskip-147.23695pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,p:{m}=_{A}{x}\vdash
B:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
H:B[m/x,{\text{refl}\;{m}}/p]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
P:{m}=_{A}{n}$}}}}}\vbox{}}}\over\hbox{\hskip
66.28146pt\vbox{\vbox{}\hbox{\hskip-66.28145pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\text{R}_{[x,p]B}^{=}({H},{P}):B[n/x,P/p]$}}}}}}$
Figure 25. Propositional Equality (Program Rules)

The most interesting aspect of TLL propositional equality lies in its
different reduction behaviors at the logical level and at the program level,
the rules of which are presented in Figure 26. Notice that in the logical
reduction rule ${\text{R}_{[x,p]A}^{=}({H},{{\text{refl}\;{m}}})\leadsto H}$,
the proof of equality must be of the form ${\text{refl}\;{m}}$ in order to
trigger reduction. This is to ensure that
$\text{R}_{[x,p]A}^{=}({H},{{\text{refl}\;{m}}})$ and $H$ have definitionally
equal types. This seems to indicate that propositional equality is
computationally relevant in the sense that an equality eliminator
$\text{R}_{[x,p]A}^{=}({H},{P})$ occurring at the program level ought to carry
around proof $P$ and reduce it to ${\text{refl}\;{m}}$. From the actual
program level reduction rule
$\text{R}_{[x,p]A}^{=}({H},{P})\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to4.09pt{\vbox to4.53pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{4.53455pt}\pgfsys@lineto{4.08897pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-8.68875pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.13pt{\vbox to3.17pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{3.1742pt}\pgfsys@lineto{3.12895pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-6.64877pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.49pt{\vbox to2.27pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{2.26727pt}\pgfsys@lineto{2.48894pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.28877pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H$ we can see that
this first impression is misleading: the program level equality eliminator
does not impose any restrictions on $P$ and immediately reduces to $H$. The
soundness of this rule is due to the fact that program reductions are not
performed under context. By the time an equality eliminator is evaluated,
logical strong normalization and canonicity guarantee the existence of a
${\text{refl}\;{m}}$ proof that $P$ is logically reducible to. In other words,
equality eliminators at the program level reduce their proofs conceptually but
not literally.

$\displaystyle\text{R}_{[x,p]A}^{=}({H},{{\text{refl}\;{m}}})\leadsto H$
$\displaystyle\text{R}_{[x,p]A}^{=}({H},{P})\leadsto\joinrel\mathrel{\mathchoice{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\displaystyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to3.68pt{\vbox to4.08pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{4.08109pt}\pgfsys@lineto{3.6801pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-7.81992pt\hbox{\set@color{$\textstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.82pt{\vbox to2.86pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{2.85677pt}\pgfsys@lineto{2.81607pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-5.98393pt\hbox{\set@color{$\scriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{\leavevmode\leavevmode\hbox{
\leavevmode\hbox to2.24pt{\vbox to2.04pt{\pgfpicture\makeatletter\hbox{\hskip
0.0pt\lower 0.0pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{{}{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{2.04053pt}\pgfsys@lineto{2.24005pt}{0.0pt}\pgfsys@closepath\pgfsys@clipnext\pgfsys@discardpath\pgfsys@invoke{
}{{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} {{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\leavevmode\hbox{\hskip-4.75995pt\hbox{\set@color{$\scriptscriptstyle\leadsto$}}}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}}
{}{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}H$
Figure 26. Propositional Equality Reduction

After recognizing that equality proofs are computationally irrelevant at the
program level, we define the erasure procedure for equality eliminators in
Figure 27 that removes the equality proof $P$ entirely. These erased programs
can be represented and evaluated much more efficiently at runtime than their
compile time logical counterparts.

$\displaystyle\displaystyle{\hbox{\hskip
156.78621pt\vbox{\hbox{\hskip-156.7862pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,p:{m}=_{A}{x}\vdash
B:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash H\sim
H^{\prime}:B[m/x,{\text{refl}\;{m}}/p]$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
P:{m}=_{A}{n}$}}}}}\vbox{}}}\over\hbox{\hskip
89.35321pt\vbox{\vbox{}\hbox{\hskip-89.35321pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\text{R}_{[x,p]B}^{=}({H},{P})\sim\text{R}_{\square}^{=}({H^{\prime}},{\square}):B[n/x,P/p]$}}}}}}$
Figure 27. Propositional Equality (Erasure Rules)

###  9.2. Subset Pairs

Leveraging the distinction between proofs and programs in TLL, we encode a
variation of $\Sigma$-types often referred to as subset types in the
verification community. For a subset type of the form
$\Sigma_{t}\\{{x:A}.{B}\\}$, its canonical inhabitant will be a pair of the
form $\\{{m},{n}\\}_{t}$ where $m$ is a relevant payload of type $A$ and $n$
is an irrelevant proof of the dependent type $B$. A common use case for subset
types is to refine programs by the properties they satisfy, essentially
carving out a subset of the original type.

The logical rules for subset types are presented in Figure 28 and the program
rules are presented in Figure 29. The side condition
${(t=\text{U})\Rightarrow(s=\text{U})}$ is required by the subset type
formation rule to prevent resource leakage via packing linear payloads into
non-linear subset pairs. Notice how in the program rule for subset pair
construction the payload $m$ is typed at the program level whereas the term
$n$ is typed at the logical level. This indicates that $m$ is computationally
relevant and $n$ is computationally irrelevant. From an erasure perspective, a
program of the form $\\{{m},{n}\\}_{t}$ is erased to
$\\{{m},{\square}\\}_{t}$.

$\displaystyle\displaystyle{\hbox{\hskip
98.085pt\vbox{\hbox{\hskip-98.085pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
A:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A\vdash
B:r$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle(t=\text{U})\Rightarrow(s=\text{U})$}}}}}\vbox{}}}\over\hbox{\hskip
35.93349pt\vbox{\vbox{}\hbox{\hskip-35.93349pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Sigma_{t}\\{{x:A}.{B}\\}:t$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
104.49767pt\vbox{\hbox{\hskip-104.49767pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Sigma_{t}\\{{x:A}.{B}\\}:t$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash m:A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:B[m/x]$}}}}}\vbox{}}}\over\hbox{\hskip
46.87062pt\vbox{\vbox{}\hbox{\hskip-46.87062pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\\{{m},{n}\\}_{t}:\Sigma_{t}\\{{x:A}.{B}\\}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
166.1518pt\vbox{\hbox{\hskip-166.15178pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,z:\Sigma_{t}\\{{x:A}.{B}\\}\vdash
C:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:\Sigma_{t}\\{{x:A}.{B}\\}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,y:B\vdash
n:C[\\{{x},{y}\\}_{t}/z]$}}}}}\vbox{}}}\over\hbox{\hskip
55.91063pt\vbox{\vbox{}\hbox{\hskip-55.91063pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\text{R}_{[z]C}^{\Sigma}({m},{[x,y]n}):C[m/z]$}}}}}}$
Figure 28. Subset Pairs (Logical Rules)
$\displaystyle\displaystyle{\hbox{\hskip
110.24768pt\vbox{\hbox{\hskip-110.24767pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Sigma_{t}\\{{x:A}.{B}\\}:t$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:B[m/x]$}}}}}\vbox{}}}\over\hbox{\hskip
52.62064pt\vbox{\vbox{}\hbox{\hskip-52.62062pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\\{{m},{n}\\}_{t}:\Sigma_{t}\\{{x:A}.{B}\\}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
190.57562pt\vbox{\hbox{\hskip-190.5756pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,z:\Sigma_{t}\\{{x:A}.{B}\\}\vdash
C:s$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\vdash
m:\Sigma_{t}\\{{x:A}.{B}\\}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x:A,y:B;\Delta_{2},x:_{r}A\vdash
n:C[\\{{x},{y}\\}_{t}/z]$}}}}}\vbox{}}}\over\hbox{\hskip
70.93066pt\vbox{\vbox{}\hbox{\hskip-70.93065pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta_{1}\mathbin{\mathaccent
0{\cdot}\cup}\Delta_{2}\vdash\text{R}_{[z]C}^{\Sigma}({m},{[x,y]n}):C[m/z]$}}}}}}$
Figure 29. Subset Pairs (Program Rules)

The following example shows applying erasure to a pair of type
${\Sigma_{\text{U}}\\{{x:\text{nat}}.{x+1=_{\text{nat}}2}\\}}$. Notice that
the proof component of the pair $({\text{refl}\;{2}})$ is completely removed
by erasure. These subset pairs realize the principle of computational
irrelevancy for program properties.

$\displaystyle\vdash\\{{1},{{\text{refl}\;{2}}}\\}_{\text{U}}\sim\\{{1},{\square}\\}_{\text{U}}:\Sigma_{\text{U}}\\{{x:\text{nat}}.{x+1=_{\text{nat}}2}\\}$

Standard dependent pairs where both components are computationally relevant
can be defined in a straightforward manner. The typing rules and semantics for
relevant pairs are fully formalized in our Coq development, but for the sake
of saving space we do not present them here.

###  9.3. Additive Pairs

To integrate the additive fragment of Linear Logic (Girard, 1987) into TLL, we
introduce $\&$-types as an extension. The logical rules are presented in
Figure 30 and the program rules are presented in Figure 31. Intuitively, a
$\&$-type of the form ${{A}\;\&_{t}{B}}$ represents the pairing of two delayed
computations of types $A$ and $B$ respectively. Canonical inhabitants of
${{A}\;\&_{t}{B}}$ are additive pairs of the form $({m},{n})_{t}$.

Of the rules depicted here, the most interesting is the program typing rule
governing the construction of additive pairs. Notice that in the premise, both
components $m$ and $n$ are typed in the same program context $\Delta$.
Furthermore, the conclusion only assumes a single copy of $\Delta$. This is a
realization of the additive fragment of Linear Logic (Girard, 1987). Due to
the fact that $m$ and $n$ are delayed computations, only one of the two will
ultimately be projected out and evaluated. So only a single copy of $\Delta$
is committed to the component that actually gets evaluated.

$\displaystyle\displaystyle{\hbox{\hskip
43.9037pt\vbox{\hbox{\hskip-43.90369pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
A:s$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
B:r$}}}}\vbox{}}}\over\hbox{\hskip
24.00049pt\vbox{\vbox{}\hbox{\hskip-24.00049pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash{{A}\;\&_{t}{B}}:t$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
46.29123pt\vbox{\hbox{\hskip-46.29121pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:A$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:B$}}}}\vbox{}}}\over\hbox{\hskip
34.6876pt\vbox{\vbox{}\hbox{\hskip-34.6876pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash({m},{n})_{t}:{{A}\;\&_{t}{B}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
27.57655pt\vbox{\hbox{\hskip-27.57654pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:{{A}\;\&_{t}{B}}$}}}\vbox{}}}\over\hbox{\hskip
22.4637pt\vbox{\vbox{}\hbox{\hskip-22.46368pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\pi_{1}\,{m}:A$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
27.57655pt\vbox{\hbox{\hskip-27.57654pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
m:{{A}\;\&_{t}{B}}$}}}\vbox{}}}\over\hbox{\hskip
22.72775pt\vbox{\vbox{}\hbox{\hskip-22.72775pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\pi_{2}\,{m}:B$}}}}}}$
Figure 30. Additive Pairs (Logical Rules)
$\displaystyle\displaystyle{\hbox{\hskip
76.41628pt\vbox{\hbox{\hskip-76.41626pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:A$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
n:B$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\triangleright
t$}}}}}\vbox{}}}\over\hbox{\hskip
40.43762pt\vbox{\vbox{}\hbox{\hskip-40.4376pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash({m},{n})_{t}:{{A}\;\&_{t}{B}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
33.32655pt\vbox{\hbox{\hskip-33.32655pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:{{A}\;\&_{t}{B}}$}}}\vbox{}}}\over\hbox{\hskip
28.2137pt\vbox{\vbox{}\hbox{\hskip-28.2137pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\pi_{1}\,{m}:A$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
33.32655pt\vbox{\hbox{\hskip-33.32655pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash
m:{{A}\;\&_{t}{B}}$}}}\vbox{}}}\over\hbox{\hskip
28.47777pt\vbox{\vbox{}\hbox{\hskip-28.47775pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma;\Delta\vdash\pi_{2}\,{m}:B$}}}}}}$
Figure 31. Additive Pairs (Program Rules)

##  10\. Implementation and Application

In this section, we describe language features implemented in the TLL compiler
with simple examples on how they can be used to effectively construct and
verify programs.

###  10.1. Linear Inductive Types

The TLL compiler supports user defined inductive types in the style of CIC
(Paulin-Mohring, 1993). Figure 32 demonstrates how a linear list can be
defined. In this definition, the arity of the llist type constructor ends in
sort L. Once llist is fully applied to an arbitrary linear type A, the
resulting type llist A will be of sort L which requires that the lists
inhabiting this type are used exactly once. So basically, by varying the sorts
of type arities and constructor arguments, we can define different
combinations of linear and non-linear inductive types.

⬇

inductive llist (A : L) : L =

| lnil

| lcons of (hd : A) (tl : llist A)

Figure 32. Linear Lists

Figure 33 defines a function 222Underscores can be used as implicit arguments
which are inferred through unification. for appending two linear lists. The
usage of the toplevel keyword program here allows the lappend function to be
applicable at the program level. Since types can only appear in
computationally irrelevant positions at the program level, the type parameter
A is quantified irrelevantly as a $\lambda{0}$ argument. Additionally, the
body of lappend is subject to linear type-checking because it can be used at
the program level. The C code emitted for lappend will reclaim the memory used
for representing xs as it is deconstructed by the match expression.

⬇

program lappend {A : L} (xs : llist A) : llist A $⊸$ llist A =

ln ys $⇒$ match xs with

| lnil $⇒$ ys

| lcons x xs $⇒$ lcons x (lappend _ xs ys)

end

Figure 33. Program for Appending Linear Lists

After a program has been defined, theorems regarding its properties can be
proven at the logical level using the logical keyword. Figure 34 shows a proof
333The notation rew [x, p $⇒$ A] P in H is the propositional equality
eliminator $\text{R}_{[x,p]A}^{=}({H},{P})$. that the logical length of two
lists appended together by lappend is equal to the sum of their individual
lengths. Notice that the llen function here is a logical specification: it
cannot be used at the program level for actual computations. If llen were to
exist relevantly at the program level, the element hd dropped without usage in
the lcons case would cause memory leakage. Basically, terms declared with the
logical keyword are not subject to linear type checking and are pruned during
the erasure phase of the compiler.

⬇

logical llen {A : L} (xs : llist A) : nat =

match xs with

| lnil $⇒$ 0

| lcons hd tl $⇒$ 1 + llen _ tl

end

logical lappend_llen (A : L) (xs ys : llist A) :

llen _ (lappend _ xs ys) $≡$ (llen _ xs) + (llen _ ys) =

match xs as xs0 in llen _ (lappend _ xs0 ys) $≡$ llen _ xs0 + llen _ ys with

| lnil $⇒$ refl

| lcons x xs0 $⇒$

rew [ n, _ $⇒$ S (llen _ (lappend _ xs0 ys)) $≡$ S n ]

lappend_llen _ xs0 ys in refl

end

Figure 34. Logical Proofs Relating Append and Length

The example that was just shown is a form of extrinsic verification. In this
style of verification, an unverified program is first written using standard
programming techniques. After the program has been fully constructed, its
properties are then stated and proven as theorems external to the program.

Taking advantage of dependent types, programs can also be verified in an
intrinsic manner where data and proofs are tightly integrated. Consider length
indexed linear vector defined in Figure 35. The constructors lNil and lCons of
this inductive type carry irrelevant proofs that the indexing natural number n
accurately characterizes the length of the constructed vector. So if a vector
is known to be of type lvec n A, we can trust that its length must be n.

⬇

inductive lvec (n : nat) (A : L) : L =

| lNil of {e : 0 $≡$ n}

| lCons of {n0 : nat} {e : S n0 $≡$ n} (hd : A) (tl : lvec n0 A)

Figure 35. Linear Length Indexed Vectors

A program for appending linear vectors is given in Figure 36. We can see
immediately from the type of the output lvec (m + n) A that its length must be
exactly the sum of the lengths of its inputs. Compared to the extrinsic
approach, intrinsic verification can help to guide the process of program
construction itself as the tightly integrated proofs serve as precise
interfaces that rule out incorrect programs.

⬇

program vappend {m n : nat} {A : L} (xs : lvec m A) : lvec n A $⊸$ lvec (m +
n) A =

ln ys $⇒$ match xs with

| lNil e $⇒$ rew [ m0, _ $⇒$ lvec (m0 + n) A ] e in ys

| lCons n0 e hd tl $⇒$

rew [ m0, _ $⇒$ lvec (m0 + n) A ] e in

lCons (n0 + n) refl hd (vappend _ _ _ tl ys)

end

Figure 36. Program for Appending Linear Vectors

The computational relevancy mechanism of TLL allows irrelevant constructor
arguments to be safely erased. For lvec in particular, constructor arguments
surrounded by braces are erased. The structure of lvec after erasure is
identical to llist. If lvec was defined verbatim in Coq, then the n0 argument
of lCons would not be erased because nat is in the Set universe.

###  10.2. Sort-Polymorphism

In TLL, non-linear types and linear types are unambiguously grouped in sorts U
and L respectively as shown through the sort uniqueness theorem (Theorem 3).
This means that multiple versions of equivalent functions may need to be
defined at different sorts, causing large amounts of code duplication.
Consider the polymorphic identity functions shown in Figure 37. The first
function idU is polymorhpic over non-linear types and the second idL is
polymorphic over linear types.

⬇

program idU {A : U} (x : A) : A = x

program idL {A : L} (x : A) : A = x

Figure 37. Sort Monomorphic Identity Functions

In order to reduce code duplication, we implement sort-polymorphism in the TLL
compiler. Toplevel declarations are allowed to quantify over sorts using sort
variables. We refer to these sort quantified declarations as sort-polymorphic
schemes. Figure 38 shows how a sort-polymorphic identity function can be
defined. The id<s> scheme is parameterized by sort variable s which is then
used by Type<s> to refer to the sort of type A generically.

⬇

program id<s> {A : Type<s>} (x : A) : A = x

Figure 38. Sort Polymorphic Identity Function

It is important to note that schemes are not proper terms in TLL. Instead, the
compiler attempts to instantiate the sort parameters of schemes with all
possible combinations of U and L. The instantiated instances that pass type
checking are elaborated into sort-monomorhpic TLL terms. Conversely, instances
that do not pass type checking are pruned. For schemes such as id where both
instantiated instances are well-typed, the compiler will essentially derive
idU and idL automatically and apply the correct version depending on the sort
of its argument.

Sort-polymorhpic schemes can also be used for deriving inductive types. Figure
39 defines a list<s,t> inductive type scheme whose elements are of sort s and
that itself is of sort t. The llist type presented in Section 10.1 can be
viewed as the instantiated instance list<L,L> where the elements of the list
are linear and the list itself is also linear. An interesting instance that
could be obtained from instantiating the list<s,t> scheme is list<L,U>. The
cons constructor of list<L,U> is unsound as it enables the duplication of
linear resources by first packing them into non-linear lists. To prevent such
unsound situations from occurring, the cons constructor of list<L,U> is
pruned, leaving list<L,U> with only nil as its constructor. In general,
constructors of non-linear inductive types may only take arguments which are
also non-linear. The constructors of scheme instances that do not satisfy this
criteria are pruned.

⬇

inductive list<s,t> (A : Type<s>) : Type<t> =

| nil

| cons of (hd : A) (tl : list<s,t> A)

Figure 39. Sort-Polymorhpic Lists

Figure 40 presents a length function for sort-polymorphic lists. Notice that
unlike the logical llen shown in Figure 34, the new len<s,t> function also
returns back the original input list paired with its length. This makes
len<s,t> sound for use as a computationally relevant program as the
aforementioned memory leakage problem regarding hd is no longer possible.
Furthermore, we can prove at the logical level that the list returned by
len<s,t> is indeed equal to its input. Due to the fact that the len_id<s,t>
theorem here is also sort-polymorphic, this single proof suffices to verify
len<s,t> for all valid sort variations of lists.

⬇

program len<s,t> {A : Type<s>} (xs : list<_,t> A) : nat $⊗$ list<_,t> A =

match xs with

| nil $⇒$ $⟨$0, nil$⟩$

| cons hd tl $⇒$

match len _ tl with

| $⟨$n, tl$⟩$ $⇒$ $⟨$S n, cons hd tl$⟩$

end

end

logical len_id<s,t> {A : Type<s>} (ls : list<_,t> A) : ls $≡$ snd _ _ (len _
ls) =

match ls as ls0 in ls0 $≡$ snd _ _ (len _ ls0) with

| nil $⇒$ refl

| cons x xs $⇒$ ...

end

Figure 40. Sort-Polymorhpic Length (Excerpt)

###  10.3. Dependent Session Types

The TLL compiler supports concurrency and facilitates communication between
processes using dependent session types. Each channel type
ch$\langle$P$\rangle$ is indexed with a protocol P describing the
communication that is expected to be conducted over it. Channel types are
linear, so the type system ensures that the only way to consume a channel is
to execute its indexing protocol to completion. We have formalized and proven
the soundness of these concurrency extensions in Coq, but due to space
limitations we will not present the communication calculus in this paper. The
examples presented here are meant to illustrate the applications of TLL to
concurrent programming.

#### Specification of Concurrent Algorithms

The most immediate application for dependent session types is the precise
specification of concurrent algorithms. Figure 41 demonstrates how a channel
for conducting concurrent mergesort can be specified. The protocol $⇑$(uniq _
(msort xs)) $\textrightarrow$ $\bullet$ indexing the channel type requires
that a value of the singleton type uniq _ (msort xs) be sent on the channel
before it can be closed. So any process with a channel of the type
cmsort_ch<t>(xs) is expected to send a list that is logically equal to xs
sorted by the sequential implementation of mergesort msort<t>.

⬇

inductive uniq<t> (A : Type<t>) (a : A) : Type<t> =

| Uniq of (m : A) {pf : m $≡$ a}

logical cmsort_ch<t> (xs : list<_,t> nat) : L =

ch$⟨$ $⇑$(uniq _ (msort xs)) $→$ $\bullet$ $⟩$

Figure 41. Protocol Specification for Concurrent Mergesort

Figure 42 presents a worker function utilizing a channel c of type
cmsort_ch<t>(zs0). A list is expected to be sent on channel c along with a
proof that it is exactly equal to zs0 sorted by the sequential implementation.
Notice in the splitting case for cmsort_worker<t>, two child-processes are
spawned by fork to carry out sorting for the list halves xs0 and ys0 in a
concurrent manner. The results of the child-processes are communicated back to
their parent-process through the channels r1 and r2 which are of types
cmsort_ch<t>(xs0) and cmsort_ch<t>(ys0) respectively. This means that the
lists xs1 and ys1 received from r1 and r2 come with proofs that they are
logically equal to msort xs0 and msort ys0. Finally, the merged list zs1 is
sent on channel c with a proof that it is equal to the original input zs0
sorted sequentially.

⬇

program cmsort_worker<t> (zs0 : list<_,t> nat) : cmsort_ch<t> zs0 $⊸$ IO unit
=

ln c $⇒$

...

let r1 $⇐$ fork (r1 : cmsort_ch xs0) in cmsort_worker xs0 r1 in

let r2 $⇐$ fork (r2 : cmsort_ch ys0) in cmsort_worker ys0 r2 in

let $⟨$msg1, r1$⟩$ $⇐$ recv r1 in

let $⟨$msg2, r2$⟩$ $⇐$ recv r2 in

match msg1 with Uniq xs1 pf1 $⇒$

match msg2 with Uniq xs2 pf2 $⇒$

let zs1 = merge xs1 xs2 in

let c $⇐$ send c (Uniq zs1 ...)

in close r1; close r2; close c

end end

...

Figure 42. Verified Concurrent Mergesort (Excerpt)

#### Implicit Secrecy Synchronization

The dependent session types found in the TLL compiler have access to the same
computational irrelevancy and erasure mechanism enjoyed by
$\lambda{0}$-programs. For instance, ${{\Uparrow}\\{{x:A}\\}\rightarrow{B}}$
is a protocol which expects to send a computationally irrelevant message $x$
of type $A$ then continue as protocol $B$. After erasure, the message sent in
place of $x$ is replaced by $\square$. At first glance, sending and receiving
irrelevant messages seem to be meaningless as $\square$ communicates no
information between sender and receiver. However, one must remember that these
irrelevant message can still be used to instantiate protocols, so a form of
implicit synchronization can be achieved without actually sending messages
across the channel.

⬇

logical DH (p g : nat) : proto =

$⇑${a : nat} $→$ $⇑$(A : nat) $→$ $⇑${ A $≡$ pow g a $\%$ p } $→$

$⇓${b : nat} $→$ $⇓$(B : nat) $→$ $⇓${ B $≡$ pow g b $\%$ p } $→$ $\bullet$

Figure 43. Diffie-Hellman Session Protocol

Figure 43 demonstrates how computational irrelevancy can be used to encode the
Diffie-Hellman key exchange (Diffie and Hellman, 1976) as a session type. The
parameters p and g are public values that both parties agree on. From Alice’s
perspective, she first sends her secret value a as an irrelevant message to
initialize her half of the protocol. Next, her public value A is sent as a
relevant message to Bob along with a proof that A is correctly computed from
values p, g and a. At this point, Alice has finished sending messages and
waits for messages from Bob to complete the key exchange. She first receives
Bob’s secret b as an irrelevant message which initializes his half of the
protocol. Later, Bob’s public value B is received as a relevant message along
with a proof that B is correctly computed from value p, g and b. Notice that
between Alice and Bob, only the relevant messages A and B will be exchanged at
runtime. The secret values a and b and other correctness proofs will be pruned
by erasure because they are irrelevant. Basically, computational irrelevancy
has allowed us to synchronize values implicitly while also maintaining their
secrecy.

⬇

program alice (a : nat) (p g : nat) (ch : ch$⟨$ DH p g $⟩$) : IO unit =

let ch $⇐$ send ch a in

let ch $⇐$ send ch (pow g a $\%$ p) in

let ch $⇐$ send ch refl in

let $⟨${b}, ch$⟩$ $⇐$ recv ch in

let $⟨$B, ch$⟩$ $⇐$ recv ch in

let $⟨${pf}, ch$⟩$ $⇐$ recv ch in

let s = pow B a $\%$ p in

close ch

program bob (b : nat) (p g : nat) (ch : hc$⟨$ DH p g $⟩$) : IO unit =

let $⟨${a}, ch$⟩$ $⇐$ recv ch in

let $⟨$A, ch$⟩$ $⇐$ recv ch in

let $⟨${pf}, ch$⟩$ $⇐$ recv ch in

let ch $⇐$ send ch b in

let ch $⇐$ send ch (pow g b $\%$ p) in

let ch $⇐$ send ch refl in

let s = pow A b $\%$ p in

close ch

Figure 44. Alice (holder of secret a) and Bob (holder of secret b)

Two simple programs alice and bob implementing the DH key exchange are
presented in Figure 44. In this definition, the secret value b that alice
receives from bob is computationally irrelevant. She can only use b in
conjunction with pf of type B $\equiv$ pow g b $\%$ p at the logical level for
hypothetical reasoning since b will not actually be sent to her at runtime.
Likewise, bob does not gain access to a computationally relevant copy of a
either. One can even inspect the intermediate representation (and C code)
generated for alice and bob by the compiler to confirm that secret values are
not transmitted. In fact, the generated code simply assigns $\square$ to b and
a for alice and bob respectively. Furthermore, the ability to type check alice
and bob independently of each other enables modular and scalable software
development.

The RSA encryption algorithm (Rivest et al., 1978) can also be encoded as a
session type in a similar manner by using computational irrelevancy to specify
the relationship between public keys and private keys. We present a
specification of the RSA protocol and a client-server pair implementing the
protocol in the appendix.

##  11\. Related Work

###  11.1. Computational Relevancy

Over the years, a number of mechanisms have been proposed for specifying
computational relevancy and program extraction. The Dependent ML (DML) of Xi
(Xi, 2007) uses a stratified language where the static fragment is irrelevant
and the dynamic fragment is relevant. A special class of indexed singleton
types carries information between the statics and the dynamics. Miquel
(Miquel, 2001) introduces the Implicit Calculus of Constructions (ICC) which
extends the standard Calculus of Constructions of Coquand (Coquand and Huet,
1988) with intersection types. Intersection types allow implicitly quantified
terms to be instantiated with hypothetical arguments that are not explicitly
present in the syntax tree. ICC programs essentially never carry around
irrelevant terms in the first place. Due to the fact that these instantiating
arguments must be synthesized spontaneously without additional information
from the syntax tree, type checking for ICC is undecidable. Barras and
Bernardo (Barras and Bernardo, 2008) develop a decidable variation of ICC
(ICC*) by requiring explicit instantiations for implicit quantifiers. An
erasure procedure is then carried out to remove the arguments of implicit
instantiations.

From a computational relevancy perspective, TLL can be viewed as an
integration of DML style stratification and ICC* style implicit
quantification. On the one hand, stratification distinguishes proofs from
programs in a straightforward manner that enforces types and assumed axioms to
always be irrelevant. Additionally, the operational semantics of the two
levels can be tailored to better facilitate reasoning and computation
independently of each other. On the other hand, implicit quantifications allow
for Martin-Löf style dependency (Martin-Löf, 1975) which is more expressive
than DML style dependency.

###  11.2. Combining Dependency and Linearity

Linear types are a class of type systems inspired by Girard’s sub-structural
Linear Logic (Girard, 1987). Girard notices that the weakening and contraction
rules of classical logic when restricted carefully, give rise to a new logical
foundation for reasoning about resources. Wadler (Wadler, 1990) applies an
analogous restriction to variable usage in simple type theory, leading to the
development of linear type theory where expressions respect resources.
Programming languages featuring linear types (Bernardy et al., 2017) or
affine-like types (The Rust teams, 2022) have been implemented, allowing
programmers to write resource safe software in practical applications.

Work has been done to enrich linear type theories with dependent types.
Cervesato and Pfenning (Cervesato and Pfenning, 2002) extend LF (Harper et
al., 1993) with linear types as LLF, being first to demonstrate that
dependency and linearity can coexist within a type theory. The ATS programming
language (Xi, 2010) extends DML style dependent types with linear types to
facilitate safe effectful programming. Vákár (Vákár, 2014) presents a
dependent linear type theory ILDTT with an underlying categorical semantics.
Krishnaswami et al. (Krishnaswami et al., 2015) introduce a dependent linear
type theory LNLD based on Benton’s (Benton, 1994) prior work of mixed linear
and non-linear calculus. Although LNLD also employs a stratified type system,
the stratification here is not used for specifying computational relevancy.
Instead, the stratification of LNLD is used for separating linear types from
non-linear types and Miquel style intersection types are used for encoding
computational relevancy.

The works described so far all prohibit types from depending on linear terms
in order to prevent resource duplication within types. Luo and Zhang (Luo and
Zhang, 2016) are the first to describe a system where linear dependency is
allowed. To accomplish this, they introduce the notion of essential linearity
which points out that types are hypothetical entities so linear terms
occurring inside types should not contribute to overall resource consumption.
Our work is inspired by the idea of essential linearity and also supports
linear dependency which allows one to prove theorems regarding linear
programs.

Based on initial ideas of McBride (McBride, 2016), Atkey’s QTT (Atkey, 2018)
uses semi-ring annotations to track variable occurrence, simulating
computational relevancy, linear types and affine types within a unified
framework. The heap semantics analysis of Choudhury et al. (Choudhury et al.,
2021) show that QTT requires a form of reference counting to garbage collect
unneeded resources at runtime. The soundness theorems for our heap semantics
guarantee TLL programs to be memory clean without runtime garbage collection.

##  12\. Conclusion and Future Work

TLL is a two-level dependent type theory that aims to characterize the nature
of proofs and programs faithfully. Hosting a structural type system that is
reminiscent of Martin-Löf type theory (Martin-Löf, 1975), the logical level
derives hypothetical objects such as proofs and types which are
computationally irrelevant. The program level uses the types and proofs
derived at the logical level to realize a Linear Logic (Girard, 1987) inspired
type system. Programs constructed using the program level rules can be freely
reflected into the logical level for hypothetical reasoning. We develop an
erasure procedure for removing irrelevant terms occurring inside programs and
show that programs extracted this way maintain computational productivity.
Through a heap semantics analysis we prove that extracted TLL programs run
memory clean.

We plan to investigate what additional extensions are possible with the
additional flexibility afforded to us by TLL’s stratified design. Currently,
we have extended TLL with session type based concurrency and intend to present
a detailed account of the calculus in the future. We are interested to see if
our approach can be refined for specifying multiparty communication and
conducting end-to-end verification of cryptographic protocols. Our ultimate
goal is to strive towards a framework that synergistically unites theorem
proving and practical programming.

## References

  * (1)
  * Atkey (2018) Robert Atkey. 2018\.  The Syntax and Semantics of Quantitative Type Theory. In _LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9–12, 2018, Oxford, United Kingdom_.  https://doi.org/10.1145/3209108.3209189
  * Barras and Bernardo (2008) Bruno Barras and Bruno Bernardo. 2008.  The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In _Foundations of Software Science and Computational Structures_ , Roberto Amadio (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 365–379.
  * Benton (1994) Nick Benton. 1994\.  A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In _CSL_.
  * Bernardy et al. (2017) Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2017.  Linear Haskell: practical linearity in a higher-order polymorphic language.  _CoRR_ abs/1710.09756 (2017).  arXiv:1710.09756 http://arxiv.org/abs/1710.09756
  * Cervesato and Pfenning (2002) Iliano Cervesato and Frank Pfenning. 2002.  A Linear Logical Framework.  _Information and Computation_ 179, 1 (2002), 19–75.  https://doi.org/10.1006/inco.2001.2951
  * Choudhury et al. (2021) Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021.  A Graded Dependent Type System with a Usage-Aware Semantics.  _Proc. ACM Program. Lang._ 5, POPL, Article 50 (jan 2021), 32 pages.  https://doi.org/10.1145/3434331
  * Coquand and Huet (1988) Thierry Coquand and Gérard Huet. 1988.  The calculus of constructions.  _Information and Computation_ 76, 2 (1988), 95–120.  https://doi.org/10.1016/0890-5401(88)90005-3
  * Coquand and Spiwack (2006) T. Coquand and A. Spiwack. 2006.  A Proof of Strong Normalisation using Domain Theory. In _21st Annual IEEE Symposium on Logic in Computer Science_. IEEE Computer Society, Los Alamitos, CA, USA, 307–316.  https://doi.org/10.1109/LICS.2006.8
  * Diffie and Hellman (1976) W. Diffie and M. Hellman. 1976.  New directions in cryptography.  _IEEE Transactions on Information Theory_ 22, 6 (1976), 644–654.  https://doi.org/10.1109/TIT.1976.1055638
  * Girard (1987) Jean-Yves Girard. 1987\.  Linear logic.  _Theoretical Computer Science_ 50, 1 (1987), 1–101.  https://doi.org/10.1016/0304-3975(87)90045-4
  * Harper et al. (1993) Robert Harper, Furio Honsell, and Gordon Plotkin. 1993\.  A Framework for Defining Logics.  _J. ACM_ 40, 1 (Jan. 1993), 143–184.  https://doi.org/10.1145/138027.138060
  * Krishnaswami et al. (2015) Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015\.  Integrating Linear and Dependent Types.  _SIGPLAN Not._ 50, 1 (Jan. 2015), 17–30.  https://doi.org/10.1145/2775051.2676969
  * Luo (1994) Zhaohui Luo. 1994\.  _Computation and Reasoning: A Type Theory for Computer Science_.  Oxford University Press, Inc., USA.
  * Luo and Zhang (2016) Zhaohui Luo and Y Zhang. 2016.  _A Linear Dependent Type Theory_.  69–70.
  * Martin-Löf (1975) Per Martin-Löf. 1975\.  An Intuitionistic Theory of Types: Predicative Part.  In _Logic Colloquium ’73_ , H.E. Rose and J.C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 73–118.  https://doi.org/10.1016/S0049-237X(08)71945-1
  * McBride (2016) Conor McBride. 2016\.  I Got Plenty o’ Nuttin’. In _A List of Successes That Can Change the World_.
  * Miquel (2001) Alexandre Miquel. 2001\.  The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In _Typed Lambda Calculi and Applications_ , Samson Abramsky (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 344–359.
  * Paulin-Mohring (1993) Christine Paulin-Mohring. 1993\.  Inductive definitions in the system Coq rules and properties. In _Typed Lambda Calculi and Applications_ , Marc Bezem and Jan Friso Groote (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 328–345.
  * Rivest et al. (1978) R. L. Rivest, A. Shamir, and L. Adleman. 1978.  A Method for Obtaining Digital Signatures and Public-Key Cryptosystems.  _Commun. ACM_ 21, 2 (feb 1978), 120–126.  https://doi.org/10.1145/359340.359342
  * The Coq Development Team (2020) The Coq Development Team. 2020\.  _The Coq Proof Assistant, version 8.11.0_.  https://doi.org/10.5281/ZENODO.3744225
  * The Rust teams (2022) The Rust teams. 2022\.  _Rust Programming Language_.  http://www.rust-lang.org/
  * Turner and Wadler (1999) David N. Turner and Philip Wadler. 1999.  Operational interpretations of linear logic.  _Theoretical Computer Science_ 227, 1 (1999), 231–248.  https://doi.org/10.1016/S0304-3975(99)00054-7
  * Vákár (2014) Matthijs Vákár. 2014\.  Syntax and Semantics of Linear Dependent Types.  _CoRR_ abs/1405.0033 (2014).  arXiv:1405.0033 http://arxiv.org/abs/1405.0033
  * Wadler (1990) P. Wadler. 1990\.  Linear Types can Change the World!. In _Programming Concepts and Methods_.
  * Xi (2007) Hongwei Xi. 2007\.  Dependent ML An approach to practical programming with dependent types.  _Journal of Functional Programming_ 17, 2 (2007), 215–286.  https://doi.org/10.1017/S0956796806006216
  * Xi (2010) Hongwei Xi. 2010\.  _The ATS Programming Language_.  http://www.ats-lang.org/