text:
\subsection{\@startsection{subsection}{2}{\z@}{-2\p@ \@plus -4\p@ \@minus -4\p@}{-0.5em \@plus -0.22em \@minus -0.1em}{\normalfont\normalsize\bfseries}}
  \makeatother

\renewcommand{\paragraph}[1]{\noindent {\bf #1}}
\fi

  \abovedisplayskip.50ex
  \belowdisplayskip.50ex
  \abovedisplayshortskip.50ex
  \belowdisplayshortskip.50ex

 \usepackage[font={small}]{caption, subfig}

 \renewcommand{\figurename}{Fig.}
 \renewcommand{\tablename}{Tab.}

 \setlength{\abovecaptionskip}{1ex}
 \setlength{\belowcaptionskip}{1ex}
 \setlength{\floatsep}{1ex}
 \setlength{\textfloatsep}{1ex}

\usepackage{paralist}

\newcommand{\keywd}[1]{\mathtt{#1}}
\newcommand{\mathrm{KPER}}{\mathrm{KPER}}
\newcommand{\myread}[1]{!{#1}}
\newcommand{\wcpo}[1]{$\omega$-cpo}
\newcommand{\wcpos}[1]{$\omega$-cpos}
\newcommand{\myref}[1]{\keywd{ref}(#1)}
\newcommand{{-}}{{-}}
\newcommand{\sq}[4]{\tensor*[^{#1}_{#2}]{\Diamond}{^{#3}_{#4}}}
\newcommand{\Diamond}{\Diamond}
\newcommand{\intt}[1]{\textit{int}(#1)}
\newcommand{\effto}[1]{\stackrel{#1}{\to}}
\newcommand{\textit{wrong}}{\textit{wrong}}
\newcommand{\unitt}[1]{\textit{unit}(#1)}
\newcommand{\sqsubseteq}{\sqsubseteq}
\newcommand{\operatorname{QPER}}{\operatorname{QPER}}
\newcommand{\operatorname{supp}}{\operatorname{supp}}
\newcommand{\booll}[1]{\textit{bool}(#1)}
\newcommand{\reff}[1]{\textit{loc}(#1)}
\newcommand{\prodd}[1]{\textit{pair}(#1)}
\newcommand{\funn}[1]{\textit{fun}(#1)}
\newcommand{\mathrel{<:}}{\mathrel{<:}}
\newcommand{\keywd{skip}}{\keywd{skip}}
\newcommand{\keywd{while}}{\keywd{while}}
\newcommand{\rightharpoondown}{\rightharpoondown}
\newcommand{\keywd{do}}{\keywd{do}}
\newcommand{\keywd{if}}{\keywd{if}}
\newcommand{\keywd{then}}{\keywd{then}}
\newcommand{\keywd{else}}{\keywd{else}}
\newcommand{\keywd{:=}}{\keywd{:=}}
\newcommand{\keywd{=}}{\keywd{=}}
\newcommand{\keywd{;}}{\keywd{;}}
\newcommand{\keywd{true}}{\keywd{true}}
\newcommand{\keywd{false}}{\keywd{false}}
\newcommand{\mx}[1]{\keywd{#1}}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{[\![}{[\![}
\newcommand{]\!]}{]\!]}
\newcommand{\lift}[1]{\lceil #1 \rceil}
\newcommand{\mathbb{V}}{\mathbb{V}}
\newcommand{\mathbb{Z}}{\mathbb{Z}}
\newcommand{\mathbb{B}}{\mathbb{B}}
\newcommand{\mathit{Stores}}{\mathit{Stores}}
\newcommand{\mathit{Stacks}}{\mathit{Stacks}}
\newcommand{\mathbb{N}}{\mathbb{N}}
\newcommand{\keywd{int}}{\keywd{int}}
\newcommand{\keywd{ref}}{\keywd{ref}}
\newcommand{\myexp}[1]{#1\ \texttt{exp}}
\newcommand{\myexp{\inttype}}{\myexp{\keywd{int}}}
\newcommand{\myexp{\keywd{bool}}}{\myexp{\keywd{bool}}}
\newcommand{\texttt{com}}{\texttt{com}}
\newcommand{\keywd{bool}}{\keywd{bool}}
\newcommand{\keywd{unit}}{\keywd{unit}}
\newcommand{\keywd{()}}{\keywd{()}}
\newcommand{\mquote}[1]{\mathtt{#1}}
\newcommand{\mathrel{bop}}{\mathrel{bop}}
\newcommand{\mathrel{op}}{\mathrel{op}}
\newcommand{\mathrel{lop}}{\mathrel{lop}}
\newcommand{\keywd{not}}{\keywd{not}}
\newcommand{: =}{: =}
\newcommand{\mathbb{T}}{\mathbb{T}}
\newcommand{\mathbb{F}}{\mathbb{F}}
\newcommand{\singleton}[1]{\{#1\}}
\newcommand{\mathbb{L}}{\mathbb{L}}
\newcommand{\dom}[1]{\mathrm{dom}({#1})}
\newcommand{\cod}[1]{\mathrm{cod}({#1})}

\newcommand{\vspace{1.5ex}}{\vspace{1.5ex}}
\newcommand{\quad\quad}{\quad\quad}
\newcommand{\quad\quad\quad}{\quad\quad\quad}
\newcommand{\stackrel{\mathit{def}}{=}}{\stackrel{\mathit{def}}{=}}

\newcommand{\rom}[1]{{\rm #1}}

\newcommand{\begin{array}}{\begin{array}}
\newcommand{\end{array}}{\end{array}}
\newcommand{\lz}[1]{\makebox[1.5in][r]{$#1$}}
\newcommand{\rz}[1]{\makebox[3in][l]{$#1$}}

\newcommand{\why}[1]{\quad\quad\mbox{\{ #1 \}}}

\newcommand{\centre}[1]{\[\makebox[0em]{$\begin{array}{c} #1 \end{array}$}\]}
\newcommand{\centretran}[1]{\[\makebox[0em]{$\begin{array}{rcl} #1 \end{array}$}\]}
\newcommand{\textit{id}}{\textit{id}}

\newenvironment{syntaxrules}{\[\begin{array}{l@{\quad\quad}lcl}}{\end{array}\]}
\newenvironment{unnamedsyntaxrules}{\[\begin{array}{lcl}}{\end{array}\]}
\newenvironment{typerules}{\[\begin{array}{c}}{\end{array}\]}
\newenvironment{reductions}{\[\begin{array}{l@{\quad\quad}lcl}}{\end{array}\]}
\newenvironment{reductionsif}{\[\begin{array}{l@{\quad\quad}lcl@{\quad\quad}l}}{\end{array}\]}
\newenvironment{translation}{\[\begin{array}{rcl}}{\end{array}\]}
\newenvironment{derivation}{\[\begin{array}{ll}}{\end{array}\]}
\newenvironment{equations}{\[\begin{array}{c@{\quad\quad}c}}{\end{array}\]}
\newenvironment{fig}
\begin{minipage}{\textwidth}}{\end{minipage}\paus
}
\newcommand{\squelch}[1]{}
\newcommand{\myremark}[1]{\par***** NOTE ******* #1\par}

\newcommand{\ipushval}[1]{\texttt{pushc}\ #1}
\newcommand{\ipushvar}[1]{\texttt{pushvar}\ #1}
\newcommand{\ipop}[1]{\texttt{pop}\ #1}
\newcommand{\mathrel{iop}}[1]{\texttt{binop}_{#1}}
\newcommand{\iif}[1]{\texttt{brtrue}\ #1}
\newcommand{\texttt{halt}}{\texttt{halt}}
\newcommand{S}{S}
\newcommand{\sigma}{\sigma}
\newcommand{\mconfig}[1]{\langle #1 \rangle}
\newcommand{\mstep}[3]{[#1];\mconfig{#2}\to \mconfig{#3}}
\newcommand{\multistep}[3]{[#1];\mconfig{#2}\to^{*} \mconfig{#3}}
\newcommand{\meval}[3]{[#1];\mconfig{#2}\Downarrow \mconfig{#3}}
\newcommand{\hspace{1cm}\hspace*{\fill}}{\hspace{1cm}\hspace*{\fill}}
\newcommand{\[\hspace*{\fill}\prooftree}{\[\hspace*{\fill}\prooftree}
\newcommand{\endprooftree\hspace*{\fill}\]}{\endprooftree\hspace*{\fill}\]}
\newcommand{\endprooftree\hspace{1cm}\hspace*{\fill}\prooftree}{\endprooftree\hspace{1cm}\hspace*{\fill}\prooftree}
\newcommand{\endprooftree\hspace*{\fill}\]\smallskip \[\hspace*{\fill}\prooftree}{\endprooftree\hspace*{\fill}\]\smallskip \[\hspace*{\fill}\prooftree}
\newcommand{\lind}[1]{\mathcal{L}_{#1}}
\newcommand{\diverges}[1]{\mathcal{D}_{#1}}

\newcommand{\vfix}[3]{\keywd{rec}\:{#1}\:{#2} = {#3}}
\newcommand{\letin}[2]{\keywd{let}\:{#1}\!\Leftarrow\!{#2}\:\keywd{in}\:}
\newcommand{\letrec}[3]{\keywd{let\ rec}\ {#1\ #2}\!\Leftarrow\!{#3}\ \keywd{in}\ }
\newcommand{\opletrec}[3]{\keywd{let\ rec}}
\newcommand{\lettwoin}[4]{\keywd{let}\:{#1}\!\Leftarrow\!{#2};{#3}\!\Leftarrow\!{#4}\:\keywd{in}\:}
\newcommand{\tlet}[3]{\keywd{let}\  #1 \Leftarrow #2\ \keywd{in}\ #3}
\newcommand{\valof}[1]{\keywd{val}\:{#1}}
\newcommand{\app}[2]{{#1}\:{#2}}
\newcommand{\abs}[2]{\lambda{#1}.\:{#2}}
\newcommand{\tabs}[2]{\Lambda{#1}.{#2}}
\newcommand{\tapp}[2]{{#1}_{#2}}
\newcommand{\proj}[2]{\pi_{#1}{#2}}
\newcommand{\tinj}[2]{\keywd{in}_{#1}^{#2}}
\newcommand{\inj}[1]{\keywd{in}_{#1}}
\newcommand{\einj}[1]{\keywd{in}_{#1}}
\newcommand{\fold}[2]{\keywd{fold}_{#1}\:{#2}}
\newcommand{\unfold}[1]{\keywd{unfold}\:{#1}}
\newcommand{\alloc}[1]{\keywd{ref}\:{#1}}
\newcommand{\deref}[1]{!{#1}}
\newcommand{\assign}[2]{{#1}:={#2}}
\newcommand{\throw}[1]{\keywd{raise}\:{#1}}
\newcommand{\catch}[3]{{#1}\:\keywd{handle}\:{#2}\Rightarrow{#3}}
\newcommand{\try}[5]{\keywd{try}\:{#1}\Leftarrow{#2}\:\keywd{handle}\:#3 . #4\:\keywd{in}\:{#5}}
\newcommand{\scatch}[2]{#1 \: \keywd{handle}\: #2}
\newcommand{\stry}[4]{\keywd{try}\: #1 \Leftarrow #2 \:\keywd{catch}\:#3\:\keywd{in}\:#4}
\newcommand{\mycase}[1]{\texttt{case}\: #1\:\texttt{of}}
\newcommand{\wrap}[1]{\texttt{wrap}\:{#1}}
\newcommand{\unwrap}[1]{\texttt{unwrap}\:{#1}}
\newcommand{\encap}[1]{\texttt{encap}\:{#1}}
\newcommand{k}{k}
\newcommand{L}{L}
\newcommand{\mathcal{L}}{\mathcal{L}}
\newcommand{\locsin}[1]{\mathrm{locs}({#1})}
\newcommand{\rdsin}[1]{\mathrm{rds}({#1})}
\newcommand{\wrsin}[1]{\mathrm{wrs}({#1})}
\newcommand{\alsin}[1]{\mathrm{als}({#1})}
\newcommand{\select}[2]{{#1}|_{#2}}
\newcommand{\uplus}{\uplus}
\newcommand{\equalon}[1]{=_{#1}}
\newcommand{\ifz}[1]{\keywd{iszero}\:{#1}}
\newcommand{\myif}[3]{\keywd{if}\ #1\ \keywd{then}\ #2\
  \keywd{else}\ #3}
\newcommand{{\keywd{let}\ }}{{\keywd{let}\ }}
\newcommand{{\Leftarrow}}{{\Leftarrow}}
\newcommand{{\ \keywd{in}\ }}{{\ \keywd{in}\ }}
\newcommand{\ttype}[2]{T_{#1}\,#2}
\newcommand{\varepsilon}{\varepsilon}
\newcommand{\mathrm{rds}}{\mathrm{rds}}
\newcommand{\mathrm{wrs}}{\mathrm{wrs}}
\newcommand{\mathrm{als}}{\mathrm{als}}
\newcommand{\sing}[1]{\{#1\}}
\newcommand{\erase}[1]{U(#1)}
\newcommand{\mathbb{P}}{\mathbb{P}}
\newcommand{\rels}[1]{\mathcal{R}_{#1}}
\newcommand{\toprel}[1]{\mathbb{T}_{#1}}
\newcommand{\botrel}[1]{\mathbb{F}_{#1}}
\newcommand{\diagrel}[1]{\Delta_{#1}}
\renewcommand{\topfraction}{.8}
\newcommand{A^\circ}{A^\circ}
\newcommand{B^\circ}{B^\circ}
\newcommand{\readsg}[1]{\texttt{r}_{#1}}
\newcommand{\writesg}[1]{\texttt{w}_{#1}}
\newcommand{\Sigma}{\Sigma}
\newcommand{\approx}{\approx}
\newcommand{\Downarrow}{\Downarrow}
\newcommand{\bot}{\bot}
\newcommand{\fullonly}[1]{}
\newcommand{\Rule}[4]{\ensuremath{\makebox[1cm]{\hfill {\rm #1}}
    \,\dfrac{#2}{#3}\,\,{#4}}}
\newcommand{\rrule}[5]{\ensuremath{\makebox[#1]{\hfill {\rm #2}}
    \,\dfrac{#3}{#4}\,\,{#5}}}
\newcommand{\Extend}[2]{{#1}\downharpoonright^{#2}}
\newcommand{\rrulesub}[7]{\ensuremath{\makebox[#1]{\hfill {\rm #2}}_{\makebox[#3]{\hfill {\rm #4}}} \,\dfrac{#5}{#6}\,\,{#7}}}
\newcommand{\Halfrule}[4]{\ensuremath{\makebox[0.5cm]{\hfill {\rm #1}}
    \,\dfrac{#2}{#3}\,\,{#4}}}
\newcommand{\RuleTwo}[4]{\ensuremath{\makebox[2cm]{\hfill {\rm #1}}
    \,\dfrac{#2}{#3}\,\,{#4}}}
\newcommand{\RuleTwofive}[4]{\ensuremath{\makebox[2.5cm]{\hfill {\rm #1}}
    \,\dfrac{#2}{#3}\,\,{#4}}}
\newlength{\lruleZeroname}
\setlength{\lruleZeroname}{0cm}
\newcommand{\RuleZero}[4]{\ensuremath{\makebox[\lruleZeroname]{\hfill {\rm #1}}
    \,\dfrac{#2}{#3}\,\,{#4}}}
\newcommand{\TODO}[1]{{TODO: \emph{#1}}}
\newcommand{\ensuremath{\tau}}{\ensuremath{\tau}}
\newcommand{\regs}[1]{\mathrm{regs}({#1})}
\newcommand{\domL}[1]{\ensuremath{\mathrm{dom}}(#1)}
\newcommand{\domR}[1]{\ensuremath{\mathrm{dom}'}(#1)}
\newcommand{\dompL}[1]{\ensuremath{\mathrm{priv}}(#1)}
\newcommand{\dompR}[1]{\ensuremath{\mathrm{priv}'}(#1)}
\newcommand{\mathrm{Par}}{\mathrm{Par}}
\newcommand{\strels}[2]{\mathrm{StRel}({#1},{#2})}
\newcommand{\mathrm{Env}}{\mathrm{Env}}
\newcommand{\mathrm{Env}_\mathbb{C}}{\mathrm{Env}_\mathbb{C}}
\newcommand{\mathrm{Env}_\mathbb{P}}{\mathrm{Env}_\mathbb{P}}
\newcommand{\mathrm{fix}}{\mathrm{fix}}
\newcommand{M_{\mathrm{cnt}}}{M_{\mathrm{cnt}}}
\newcommand{M_{\mathrm{mem}}}{M_{\mathrm{mem}}}
\newcommand{M_{\mathrm{buf}}}{M_{\mathrm{buf}}}
\newcommand{M_{\mathrm{const}}}{M_{\mathrm{const}}}
\newcommand{V_{\mathrm{sum}}}{V_{\mathrm{sum}}}
\newcommand{\inv}[1]{\ensuremath{\mathrm{inv}(#1)}}
\newenvironment{myexample}%
               {\vspace{1em}{\bf Example.
               }%

               \endofproofmarker\gdef\endofproofmarker{}%
               \vspace{1em}%
               }
\newcommand{\ok}[2]{\ensuremath{{#1} \vdash {#2}\ \mathit{ok}}}
\newcommand{\eq}[1]{\mathrel{\sim_{#1}}}
\renewcommand{\P}{\ensuremath{\mathcal{P}}}
\newcommand{\ensuremath{\mathbb{Z}}}{\ensuremath{\mathbb{Z}}}
\newcommand{\ensuremath{\mathbb{B}}}{\ensuremath{\mathbb{B}}}
\newcommand{\ensuremath{\mathbf{1}}}{\ensuremath{\mathbf{1}}}
\newcommand{\ensuremath{\rho}}{\ensuremath{\rho}}
\newcommand{\ensuremath{\mathsf{r}}}{\ensuremath{\mathsf{r}}}
\newcommand{\ensuremath{\mathit{Regs}}}{\ensuremath{\mathit{Regs}}}
\newcommand{\ensuremath{\labs}}{\ensuremath{\mathbb{L}}}
\newcommand{\ensuremath{\mathit{new}}}{\ensuremath{\mathit{new}}}
\newcommand{\ensuremath{\mathbb{H}}}{\ensuremath{\mathbb{H}}}
\newcommand{\sem}[1]{\ensuremath{\llbracket {#1} \rrbracket}}
\newcommand{\semV}[1]{\ensuremath{\llceil {#1} \rrceil
}}
\newcommand{\csem}[1]{\ensuremath{\llbracket {#1}
    \rrbracket_\mathbb{C}}}
\newcommand{\psem}[1]{\ensuremath{\llbracket {#1} \rrbracket_\mathbb{P}}}
\newcommand{{\ensuremath{\mathit{nwrs}}}}{{\ensuremath{\mathit{nwrs}}}}
\newcommand{{\ensuremath{\mathit{nwrs}}}}{{\ensuremath{\mathit{nwrs}}}}
\newcommand{{\ensuremath{\mathit{nwrs}'}}}{{\ensuremath{\mathit{nwrs}'}}}
\newcommand{\mathcal{E}}{\mathcal{E}}
\newcommand{\aEff}[1]{\ensuremath{\mathit{al}_{#1}}}
\newcommand{\rEff}[1]{\ensuremath{\mathit{rd}_{#1}}}
\newcommand{\wEff}[1]{\ensuremath{\mathit{wr}_{#1}}}
\newcommand{\EffExt}[3]{\ensuremath{\Omega^{#1}_{#2}({#3})}}
\newcommand{\Prels}[3]{\ensuremath{\mathcal{R}^{#1}_{#3}({#2})}}
\newcommand{\Ext}[3]{\ensuremath{\operatorname{Ext}}^{#1}_{#3}({#2})}
\newcommand{\operatorname{Alloc}}{\operatorname{Alloc}}

\newcounter{Examplecount}
\setcounter{Examplecount}{0}
\renewenvironment{example}
{
\stepcounter{theorem} {\bf \noindent Example
\arabic{section}.\arabic{theorem} }}
{\endofproofmarker\gdef\endofproofmarker{}}
\renewenvironment{proof}{\vspace{-1mm} \noindent {\bf Proof}\quad}{\endofproofmarker\gdef\endofproofmarker{}}
\newcommand\im{\mathrm{Img}}

\newcommand{\ensuremath{\mathsf{L}}\xspace}{\mathfrak{l}}
\newcommand{\ensuremath{\ell}\xspace}{\ensuremath{\mathsf{l}}\xspace}
\newcommand\w{\ensuremath{\mathsf{w}}\xspace}
\newcommand\q{\ensuremath{\mathsf{q}}\xspace}
\newcommand{\ensuremath{\mathbb{B}}\xspace}{\ensuremath{\mathbb{B}}\xspace}
\newcommand{\ensuremath{\mathbf{W}}\xspace}{\ensuremath{\mathbf{W}}\xspace}
\newcommand{\ensuremath{\mathbf{W}_{\mathrm{Iso}}}\xspace}{\ensuremath{\mathbf{W}_{\mathrm{Iso}}}\xspace}
\newcommand\heap{\ensuremath{\mathsf{h}}\xspace}
\newcommand\heapp{\ensuremath{\mathsf{g}}}
\newcommand{\mathbb{V}}{\mathbb{V}}
\newcommand{\mathbb{C}}{\mathbb{C}}
\newcommand{\mathfrak{S}}{\mathfrak{S}}
\newcommand{\ensuremath{\mathbb{S}}\xspace}{\ensuremath{\mathbb{S}}\xspace}
\newcommand{\ensuremath{\sigma}\xspace}{\ensuremath{\sigma}\xspace}
\newcommand{\taken}[2]{\ensuremath{#1\!\! \! \upharpoonright^#2}\xspace}

\newcommand\val{\ensuremath{\mathsf{v}}\xspace}
\newcommand\vval{\ensuremath{v}\xspace}
\newcommand\fval{\ensuremath{\mathsf{f}}\xspace}
\newcommand\ffval{\ensuremath{f}\xspace}
\newcommand\cval{\ensuremath{\mathsf{c}}\xspace}
\newcommand\ccval{\ensuremath{c}\xspace}

\newcommand\pull[2]{\ensuremath{\underline{#1}_{#2}}\xspace}
\newcommand\push[2]{\ensuremath{\overline{#1}_{#2}}\xspace}
\newcommand\rel{\ensuremath{\mathrm{Rel}}\xspace}

\newcommand\Cscr{\ensuremath{\mathcal{C}}\xspace}
\newcommand\Std{\ensuremath{\mathit{Std}}\xspace}
\newcommand\Rscr{\ensuremath{\mathcal{R}}\xspace}
\newcommand\fst[1]{\ensuremath{\mathsf{fst}(#1)}\xspace}
\newcommand\Eq[1]{\ensuremath{\mathsf{Eq}(#1)}\xspace}
\newcommand{\readSet}[1]{\ensuremath{\mathcal{R}({#1})}}
\newcommand{\writeSet}[1]{\ensuremath{\mathcal{W}({#1})}}
\newcommand{\allocSet}[1]{\ensuremath{\mathcal{A}({#1})}}
\newcommand{\fr}[1]{\ensuremath{\mathsf{Fr}(#1)}\xspace}
\newcommand{\res}[2]{\ensuremath{\mathsf{Res}(#1,#2)}\xspace}
\newcommand{\ety}[2]{{#1}\mathrel{\&}{#2}}
\newcommand{\valty}[1]{#1}

\title{Abstract Effects and Proof-Relevant Logical Relations}

\author{Nick Benton\iffull\inst{1}\fi \and Martin Hofmann\iffull\inst{2}\fi  \and Vivek
Nigam\iffull\inst{3}\fi}
\institute{Microsoft Research, LMU Munich and Federal University of Para\'iba}
\squelch{
\institute{\iffull
Microsoft Research, UK, \email{nick@microsoft.com}
\and\fi
LMU, Munich, Germany,
\email{hofmann@ifi.lmu.de}
\iffull\and
Federal University of Para\'iba, Brazil, \email{vivek.nigam@gmail.com}\fi
}
}

\begin{document}
\maketitle
\begin{abstract}
  We introduce a novel variant of logical relations that maps types
 not merely to partial equivalence relations on values, as is
  commonly done, but rather to a proof-relevant generalisation
  thereof, namely setoids.
\squelch{
A setoid is like a category all of whose
  morphisms are isomorphisms (a groupoid) with the exception that no
  equations between these morphisms are required to hold.
}
  The objects of a setoid establish that values inhabit semantic
  types, whilst its morphisms
  are understood as proofs of semantic equivalence.

  The transition to proof-relevance solves two well-known
  problems caused by the use of existential quantification over future
  worlds in traditional Kripke logical relations: failure of
  admissibility, and spurious functional dependencies.

  We illustrate the novel format with two applications: a direct-style
  validation of Pitts and Stark's equivalences for ``new'' and a
  denotational semantics for a region-based effect system that
  supports type abstraction in the sense that only externally visible
  effects need to be tracked; non-observable internal modifications,
  such as the reorganisation of a search tree or lazy initialisation,
  can count as `pure' or `read only'. This `fictional purity' allows
  clients of a module soundly to validate more effect-based program
  equivalences than would be possible with traditional effect systems.
\end{abstract}
\squelch{
\category{D.3.3}{Programming Languages}{Language Constructs and Features -- Dynamic storage management}
\category{F.3.2}{Logic and Meanings of Programs}{Semantics of Programming Languages -- Denotational semantics, Program analysis}
\category{F.3.2}{Logic and Meanings of Programs}{Studies of Program Constructs -- Type structure}
\terms
Languages, Theory
\keywords
Type and effect systems, region analysis, logical relations, parametricity, program transformation
}

\iffull \else \vspace{-4mm} \fi
\section{Introduction}
\label{sec:intro}
The last decade has witnessed significant progress in modelling and
reasoning about the tricky combination of effects and higher-order
language features (first-class functions, modules, classes).  The
object of study may be ML-, Java-, or assembly-like, but the common
source of trickiness is the way effectful operations may be
\emph{partially} encapsulated behind higher-order
abstractions. Problems in semantics and verification of effectful
languages are often addressed using a range of common techniques that
includes separation and Kripke logical relations (KLRs). The
particular problem motivating the development of the proof-relevant
form of KLR introduced here is that of giving a semantics to effect
systems that accounts for partial encapsulation, though the general
construction is more broadly applicable. As we will see, direct
semantic reasoning in our model (as opposed to generic reasoning based
on refined types) also allows many of the trickiest known equivalences
concerning encapsulated store to be proved.

\squelch{One is to devise models and reasoning principles for establishing
contextual (in)equivalences
\cite{DBLP:conf/mfcs/PittsS93,DBLP:journals/corr/abs-1103-0510}. A
second is to establish equivalence between high-level and low-level
code fragments, e.g. for compiler correctness
\cite{DBLP:conf/icfp/BentonH09,DBLP:conf/popl/HurD11}. A third is to
define Hoare-style logics for showing programs satisfy
assertions \cite{DBLP:journals/corr/abs-1109-3031}. A fourth, which
we address here, is to study type systems and analyses that
can characterise particular \emph{classes} of behaviour (such as
purity) and be used to justify equivalences more generically.
}

Effect systems \cite{DBLP:conf/lfp/GiffordL86} refine conventional
types by tracking upper bounds on the side-effects of expressions.  A
series of papers, by ourselves and others
\cite{DBLP:conf/popl/KammarP12,DBLP:conf/ppdp/BentonKBH09,DBLP:conf/ppdp/BentonKBH07,DBLP:conf/aplas/BentonKHB06,DBLP:conf/icfp/ThamsborgB11},
have explored the semantics of effect systems for mutable state,
addressing not merely the correctness of analyses, but also the
soundness of effect-dependent optimizations and refactorings. An
example is the commutation of stateful computations $M$ and $N$,
subject to the condition that the sets of storage locations
potentially written by $M$ and $N$ are disjoint, and that neither
potentially reads a location that the other writes.  \squelch{If one
  gives expressions refined monadic types of the form $T_\varepsilon \tau$,
  meaning `computations returning results of type $\tau$ with
  side-effects bounded by $\varepsilon$', for a suitable choice of effect
  annotations $\varepsilon$, then effect-dependent equivalences can be
  formalized in terms of conditions on annotations. For example
  \infrule {\Gamma\vdash M:T_\varepsilon\tau \andalso \Gamma\vdash
    N:T_{\varepsilon'}\tau' \andalso \Gamma,x:\tau,y:\tau' \vdash
    P:T_{\varepsilon''}\tau''\\ \wrsin{\varepsilon}\cap
    \wrsin{\varepsilon'}=\rdsin{\varepsilon}\cap \wrsin{\varepsilon'} = \rdsin{\varepsilon'}\cap
    \wrsin{\varepsilon}=\emptyset} {\Gamma
    \vdash \begin{array}{l}\letin{x}{M}{\letin{y}{N}{P}}\\ =
      \letin{y}{N}{\letin{x}{M}{P}}\end{array} :
    T_{\varepsilon\cup\varepsilon'\cup\varepsilon''}\tau''}

\noindent
where $\rdsin{\varepsilon}$ and $\wrsin{\varepsilon}$ are the sets of possibly-read
and possibly-written variables (or regions) in $\varepsilon$.} Our primary
interest is not syntactic rules for type assignment, but rather
semantic interpretations of effect-refined types that can justify such
equivalences.  Types provide a common interface language that can be
used in modular reasoning about rewrites; types can be assigned to
particular terms by a mixture of more or less sophisticated inference
systems, or by deeper semantic reasoning. \squelch{Clearly, such a
  separation of concerns requires that the interpretation of types be
  independent of any inference system.}

A key notion in compositional reasoning about state is that of
\emph{separation}: invariants depending upon mutually disjoint parts
of the store. Intuitively, if each function with direct access to a
part preserves the corresponding invariant, then all the invariants
will be preserved by any composition of functions. Disjointness is
naively understood in terms of sets of locations.  A memory
allocator, for example, guarantees that its own private
datastructures, memory belonging to clients, and any
freshly-allocated block inhabit mutually disjoint sets of
locations. Since the introduction of fractional permissions,
separation logics often go beyond this simple model, introducing
resources that are combined with a separating conjunction, but which
are not literally interpreted as predicates on disjoint
locations. Research on `domain-specific'
\cite{DBLP:conf/tldi/KrishnaswamiBA10}, `fictional'
\cite{DBLP:conf/vstte/Dinsdale-YoungGW10,DBLP:conf/esop/JensenB12},
`subjective' \cite{leywild:scsl}, or `superficial'
\cite{krishnaswami:superficially} separation \squelch{logics and type theories}
aims to let custom notions of separable resource be used
and combined modularly. This paper presents a semantics for effect
systems supporting fictional, or `abstract', notions of both effects
and separation.

We previously interpreted effect-refined types for stateful
computations as binary relations, defined via preservation of
particular sets of store relations. This already provides some
abstraction. For example, a function that reads a reference, but whose
result is independent of the value read can soundly be counted as pure
(contrasting with models that instrument the concrete semantics). Our
models also validated the masking rule, allowing certain
non-observable effects not to appear in annotations. But here we go
further, generalizing the interpretation of regions to partial
equivalence relations (PERs). This allows, for example, a lookup
function for a set ADT to be assigned a read-but-not-write effect,
even if the concrete implementation involves non-observable writes to
rebalance an internal datastructure. Roughly, there is a PER that
relates two heaps iff they contain well-formed datastructures
representing the same mathematical set, and the ADT operations respect
this PER: looking up equal values in related heaps yields equal
booleans, adding equal values in related heaps yields new related
heaps, and so on. A mutating operation need only be annotated with a
write effect if the updated heap is potentially in a different
equivalence class from the original one. In fact, we further improve
previous treatments of write effects, via a `guarantee' condition that
explicitly captures allowable local updates. Surprisingly, this allows
the update and remove operations for our set ADT to be flagged with
\emph{just} a write effect, despite the fact that the final state of
the set depends on the initial one, exploiting the idempotence of the
updates and validating many more useful program transformations.

Moving to PERs also allows us to revisit the notion of separation,
permitting distinct abstract locations, or regions, to refer to PERs
whose footprints overlap, albeit non-observably, in memory. A module
may, for example, implement two distinct logical references using a
single physical location containing a coding (e.g. $2^i3^j$) of a pair
$(i,j)$ of integers. Or a resource allocator can keep logically
separated tokens tracking each allocated resource, acting as
permissions for deallocation, in a shared datastructure such as a
bitmap or linked list (a well-known problem in modular separation
\cite{krishnaswami:superficially}). The innovation here is a notion of independence of PERs,
capturing the situation where intersection of PERs yields a cartesian
product of quotients of the heap.

\begin{wrapfigure}{r}{.5\textwidth}
\vspace{-3mm}
\[\begin{array}{@{}l}
(T_\varepsilon Q)_\w = QPER(\{(f,f')\mid \heap,\heap'\models\w\Rightarrow\\
\ \forall R\in{\cal R}_\varepsilon(\w). \heap R \heap' \Rightarrow \heap_1 R \heap'_1 \wedge\\
\ \exists \w_1. (\w_1(r)\not= \emptyset\Rightarrow r\in \mathrm{als}(\varepsilon))\wedge  \heap_1,\heap_1'\models \w\otimes\w_1 \wedge\\
\ \heap_1 \sim_{\w_1} \heap'_1 \wedge (v,v')\in Q_{\w\otimes\w_1}\\
\ \mbox{where $(\heap_1,v)=f \heap$ and $(\heap'_1,v')= f' \heap'$\})}
\end{array}
\vspace{-2mm}
\]
\vspace{-2mm}
\caption{Earlier Kripke logical relation, extract}
\label{fig:oldklr}
\vspace{-9mm}
\end{wrapfigure}
The ideas sketched above are intuitively rather compelling, but
formally integrating them into the form of KLR we had previously used
for effect systems turns out to be remarkably
hard. Figure~\ref{fig:oldklr} shows a (tweaked) extract from an earlier
paper \cite{DBLP:conf/ppdp/BentonKBH07}. Here a world $\w$ is just a finite partial bijection between
locations, with region-coloured links; $\heap,\heap'\models \w$
simply means that for each link $(\ensuremath{\ell}\xspace,\ensuremath{\ell}\xspace')\in \w $,
$\ensuremath{\ell}\xspace\in\dom{\heap}$
and $\ensuremath{\ell}\xspace'\in\dom{\heap'}$.
Two
computations $f,f':\ensuremath{\mathbb{H}} \rightharpoondown
\ensuremath{\mathbb{H}}\times\mathbb{V}$, where $\ensuremath{\mathbb{H}},\mathbb{V}$ are
sets of heaps and values, respectively, are in the relation
$(T_\varepsilon Q)_\w$, where $\varepsilon$ is an effect and the relation $Q$ interprets a
result type, if they preserve all heap relations $R$ in a set
depending on $\varepsilon$ and $\w$, and there exists \emph{some}
disjoint world extension $\w_1$ such that the new heaps are equal on
the domain of $\w_1$, and the result values are $Q$-related at the
extended world $\w\otimes \w_1$.

The problematic part
is the existential quantification over world extensions -- the
$\exists \w_1$ on the third line -- allowing for the computations
to allocate fresh locations.
This pattern of
quantification occurs in many accounts of generativity, but
the dependence of $\w_1$ on both $\heap$ and $\heap'$ creates serious problems
if one generalizes from bijections to PERs
and tries to prove equivalences.
Roughly, one has to consider varying the initial heap in
which one computation, say $f'$, is started; the
existential then produces a \emph{different} extension $\w_2$
that is
not at all related, even on the side of $f$ where the
heap stays the same, to the $\w_1$ with which one started. The
case of bijections, where $\heap_1$ depends only on
$\heap$ (not on $\heap'$), allows one to deduce sufficient information
about the domain of $\w_1$ from the clause $\heap_1,\heap_1'\models \w\otimes\w_1$,
but this breaks down in the more abstract setting.

To fix this problem, we here
take the rather novel step of replacing the existential
quantifier in the logical relation by appropriate Skolem functions,
explicitly enforcing the correct dependencies. In the language of
type theory, this amounts to replacing an existential  with
a $\Sigma$-type. A statement like $(f,f')\in T_\varepsilon\sem{A}$ is no
longer just a proposition, but we rather have a ``set of
proofs'' $T_\varepsilon\sem{A}(f,f')$ which in particular contains
the aforementioned Skolem functions. We use an explicit version of the
exact-completion \cite{DBLP:conf/mfps/CarboniFS87,DBLP:conf/lics/BirkedalCRS98} akin to and motivated by ``setoid'' or groupoid interpretations of type theory
\cite{DBLP:conf/lics/HofmannS94,DBLP:journals/jfp/BartheCP03,DBLP:conf/cpp/Voevodsky11} to make these ideas both rigorous and more
general.

Passing from relations to proof-relevant setoids also solves other
problems. Existential quantification fails to preserve admissibility
of relations, needed to deal with general recursion, and also fails to
preserve `PERness'. The `$QPER(\cdot)$' operation in
Figure~\ref{fig:oldklr} explicitly applies an admissible and (variant)
PER closure operation; this works technically, but is very awkward to
use. We do not need such a closure here. Step indexing
\cite{DBLP:conf/esop/Ahmed06,DBLP:conf/icfp/ThamsborgB11} and the use
of continuations \cite{DBLP:conf/mfcs/PittsS93} can also deal with
admissibility.  However, step-indexing is inherently operational,
whilst continuations lose sufficient abstraction to break some program
equivalences, including commuting computations. Our third way, using
setoids, is pleasantly direct. Finally, allocation
effects are handled differently from reading and writing by the
relation in Figure~\ref{fig:oldklr}, being wired into the
quantification rather than treated more abstractly by relation
preservation. Our setoid-based formulation uses uniform machinery to
treat all effects.

We start by reviewing some preliminary definitions on syntax and
semantics of programs in Section~\ref{sec:semantics}.
Section~\ref{sec:setoids} introduces setoids, which is the setting in
which we specify in Section~\ref{test} the typed semantics and
introduce the notion of abstract effects. In
Section~\ref{sec:logical-relations} we describe proof-relevant logical
relations, prove the fundamental theorem and define observational
equivalence. Section~\ref{sec:application} demonstrates a number of
program equivalences that can be shown by using proof-revelant logical
relations. We conclude and discuss future work in
Section~\ref{sec:conclusions}.

\ifapp
\paragraph{Note:} We have elided many proofs, details of constructions
and examples. This longer version of the paper includes some of this
material in an appendix.
\else
\paragraph{Note:} We have elided many proofs, details of constructions
and examples. A longer version of the paper includes some of this
material in an appendix, and is available from the first author's
homepage.
\fi

  \squelch{A long version, possibly formalised
  will contain these details which are not hard to reconstruct
  oneself, but tedious and space-consuming to typeset.}

\section{Syntax and Semantics}
\label{sec:semantics}
We will interpret effect-refined types over a somewhat generic,
untyped denotational model for stateful computations in the category
of predomains ($\omega$-cpos).  We also introduce a meta-language
\cite{moggi1991notions}, providing concrete syntax for functions in
the model. We omit the standard details of interpreting CBV
programming languages via such a metalanguage, or proofs of adequacy,
relating the operationally induced observational (in)equivalence to
(in)equality in the model.

\paragraph{Denotational model}
\iffull
A \emph{predomain} is an $\omega$-cpo, i.e. a partial order with suprema
of ascending chains. A \emph{domain} is a predomain with a least element,
$\bot$. \squelch{We use predomains and continuous functions, rather than sets
and functions, so as to be able to interpret recursive definitions.}
Recall that $f:A\rightarrow A'$ is \emph{continuous} if it is monotone
$x\leq
y \Rightarrow f(x)\leq f(y)$ and preserves suprema of ascending
chains, i.e., $f(\sup_i x_i)=sup_i f(x_i)$. Any set is a predomain with the
discrete
order. If $X$ is a set and $A$ a predomain then
any $f:X\rightarrow A$ is continuous. A subset $U$ of a
predomain $A$ is \emph{admissible} if whenever $(a_i)_i$ is an ascending
chain in $A$ such that $a_i\in U$ for all $i$, then $\sup_i a_i\in U$,
too. If $f:X\times A\rightarrow A$ is continuous and $A$ is a domain
then one defines $f^\dagger(x)=\sup_if_x^i(\bot)$ with
$f_x(a)=f(x,a)$. One has, $f(x,f^\dagger(x))=f^\dagger(x)$ and if
$U\subseteq A$ is admissible and $f:X\times U\rightarrow U$ then
$f^\dagger:X\rightarrow U$, too. We denote a partial (continuous)
function from set (predomain) $A$ to set (predomain) $B$ by $f:A
\rightharpoondown B$.
\fi
We assume predomains $\mathbb{V}$ and $\ensuremath{\mathbb{H}}$ modelling values and heaps,
respectively. As much of the metatheory does not rely on the finer
details of how these predomains are defined, we axiomatise the
properties we use.  Firstly, we assume the existence of a set of
(concrete) locations $\mathbb{L}$ and for each $\heap\in\ensuremath{\mathbb{H}}$ a finite
set $\dom\heap\subseteq\mathbb{L}$. We also assume a constant
$\emptyset\in\ensuremath{\mathbb{H}}$, the empty heap.  If $
\heap \in \ensuremath{\mathbb{H}}, \ensuremath{\ell}\xspace \in \dom{\heap}$, then $\heap(\ensuremath{\ell}\xspace)
\in \mathbb{V}$. If $v\in
\mathbb{V}, \heap \in \ensuremath{\mathbb{H}}, \ensuremath{\ell}\xspace\in\dom{\heap}$ then $\heap[\ensuremath{\ell}\xspace{\mapsto}
v]\in\ensuremath{\mathbb{H}}$; finally $\ensuremath{\mathit{new}}(\heap,v)$ yields a pair $(\ensuremath{\ell}\xspace,\heap')$
where $\ensuremath{\ell}\xspace\in\ensuremath{\labs}$ and $\heap'\in\ensuremath{\mathbb{H}}$. These three operations
are continuous, in particular, $\heap\leq\heap'\Rightarrow
\dom\heap\subseteq \dom{\heap'}$ and the following axioms hold:
$\dom{\emptyset}=\emptyset$,
$\dom{\heap[\ensuremath{\ell}\xspace{\mapsto}v]}=\dom{\heap}$,
$(\heap[\ensuremath{\ell}\xspace{\mapsto}v])(\ensuremath{\ell}\xspace') =$ $\textit{if }\ensuremath{\ell}\xspace=\ensuremath{\ell}\xspace'\textit{
  then }v\textit{ else } \heap(\ensuremath{\ell}\xspace')$, and if
$\ensuremath{\mathit{new}}(\heap,v)=(\ensuremath{\ell}\xspace,\heap')$ then
$\dom{\heap'}=\dom{\heap}\cup\{\ensuremath{\ell}\xspace\}$ and $\ensuremath{\ell}\xspace\not\in\dom{\heap}$
and $\heap'(\ensuremath{\ell}\xspace)=v$.  Given $\mathbb{V}$ this abstract datatype can be
implemented in a number of ways, e.g., as finite maps.
We define the domain of computations $\mathbb{C}$ to be
partial continuous functions from $\ensuremath{\mathbb{H}}$ to $\ensuremath{\mathbb{H}}\times
\mathbb{V}$, the bottom element being the everywhere undefined function.

We assume that $\mathbb{V}$ embeds tuples of values, i.e., if
$v_1,\dots,v_n\in\mathbb{V}$ then $(v_1,\dots,v_n)\in\mathbb{V}$ and it is
possible to tell whether a value is of that form and in this case to
retrieve the components. We also assume that $\mathbb{V}$ embeds
continuous functions $f:\mathbb{V}\rightarrow \mathbb{C}$, i.e., if $f$ is
such a function then $\funn f\in\mathbb{V}$ and, finally, locations are
also values, i.e.\ if $\ensuremath{\ell}\xspace\in\mathbb{L}$ then $\reff\ensuremath{\ell}\xspace\in\mathbb{V}$ and
one can tell whether a value is a location or a function. A canonical
example of
such a $\mathbb{V}$ is the least solution to the predomain equation
with $\mathbb{C}=\ensuremath{\mathbb{H}}\rightharpoondown\ensuremath{\mathbb{H}}\times \mathbb{V}$ and
\(
\mathbb{V} \simeq \intt{\mathbb{Z}} + \funn{\mathbb{V}\rightarrow\mathbb{C}} +
\reff{\mathbb{L}} + \mathbb{V}^*.
\)

\paragraph{Syntax}
The syntax of untyped values and computations is:
\iffull
\[
 \begin{array}{lcl}
v & ::= & x \mid () \mid c \mid (v_1,v_2) \mid v.1 \mid v.2 \mid
\vfix{f}{x}{t} \\
t &::=& v \mid \letin{x}{t_1}{t_2}\mid v_1\,v_2 \mid
\myif{v}{t_1}{t_2} \mid
\myread{v}\mid \assign{v_1}{v_2}\mid \myref{v}
 \end{array}
\]
Here, $x$ ranges over variables and $c$ over constant
\else

\(
 \begin{array}{lcl}
v & ::= & x \mid () \mid c \mid (v_1,v_2) \mid v.1 \mid v.2 \mid
\vfix{f}{x}{t} \\
t &::=& v \mid \letin{x}{t_1}{t_2}\mid v_1\,v_2 \mid
\myif{v}{t_1}{t_2} \mid
\myread{v}\mid \assign{v_1}{v_2}\mid \myref{v}
 \end{array}
\)

\noindent
Here, $x$ ranges over variables and $c$ over constant
\fi
symbols, each of which has an associated interpretation
$\semV{c}\in\mathbb{V}$; these include numerals $\underline{n}$ with
$\semV{\underline{n}} = \intt{n}$, arithmetic operations and so on.
$\vfix{f}{x}{t}$ defines a recursive function with body $e$ and
recursive calls made via $f$; we use $\lambda x.t$ as syntactic sugar in
the
case when $f\not\in fv(t)$. Finally, $\myread{v}$ (reading) returns
the contents of location $v$, $\assign{v_1}{v_2}$ (writing) updates
location $v_1$ with value $v_2$, and $\myref{v}$ (allocating) returns a
fresh location intialised with $v$. The metatheory is simplified by
using ``let-normal form'', in which the only elimination for
computations is let, though we sometimes nest computations as
shorthand for let-expanded versions in examples.

\paragraph{Semantics}
The untyped semantics of values $\semV{v}\in\mathbb{V}\rightarrow\mathbb{V}$
and terms $\semV{t}\in\mathbb{V}\rightarrow\mathbb{C}$ are defined by an
entirely standard mutual induction, using least fixed points to
interpret recursive functions, projection from tuples for variables
and so on.
\squelch{
are given by
the recursive clauses in Figure~\ref{seme}; note the overloading of
semantic brackets for constants, values and computations.
The notation
$\eta(x)$ stands for the $i$-th projection from $\eta\in\mathbb{V}$
if $x$ is $x_i$ and $\eta[x{\mapsto}v]$ (functionally) updates the
$i$-th slot in $\eta$ when $x=x_i$.
}

\paragraph{Types}
Types are given by the grammar:
\iffull
\[
\tau ::= \keywd{unit} \mid \keywd{int}\mid A\mid\tau_1\times\tau_2\mid
\tau_1\effto\varepsilon \tau_2
\]
where $A$ ranges over semantically defined basic types (see
\else
$
\tau ::= \keywd{unit} \mid \keywd{int}\mid A\mid\tau_1\times\tau_2\mid
\tau_1\effto\varepsilon \tau_2,
$
where $A$ ranges over semantically defined basic types (see
\fi
Def.~\ref{defte}). These contain reference types possibly
annotated with regions and abstract types like lists, sets, and even
objects, again possibly refined by regions. The metavariable $\varepsilon$
represents an \emph{effect}, that is a subset of some fixed set of
elementary effects about which we say more later. The core typing
rules for values and computations are shown in
Figure~\ref{tyres}. We do not bake in type rules for
constants and effectful operations but, for a given semantic interpretation
of types, we will be able to justify adding further rules for these
primitives and, more importantly, for more complex expressions
involving them. (The rules given here incorporate
subeffecting; we expect our semantics to extend
to more general subtyping.)

\paragraph{Equations} Figure~\ref{eqth} outlines a core equational theory for
the metalanguage.  The full theory includes congruence rules for all
constructs (like that given for \texttt{rec}), all the usual beta and
eta laws and commuting conversions for conditionals as well as for
\texttt{let}.
We give
a semantic interpretation of typed equality judgements which is sound
for observational equivalence.
As with typings, further equations involving effectful computations may be
justified semantically in a particular model and added to the theory.
The core theory then allows one to
deduce new semantic equalities from already proven ones.
The equations are typed: a derivation
$\mathcal{D}$ of $\Gamma\vdash t=t':\ety{\tau}{\varepsilon}$ is canonically
associated with typing derivations $\mathcal{D}.1$ and $\mathcal{D}.2$
of $\Gamma\vdash t:\ety{\tau}{\varepsilon}$ and $\Gamma\vdash t':
\ety{\tau}{\varepsilon}$,
respectively (but note we can semantically justify extending the
type rules). The interpretation of
$\mathcal{D}$ will be a proof object certifying that the
interpretations of $\mathcal{D}.1$ and $\mathcal{D}.2$ are
semantically equal which then implies (Theorem~\ref{obseq}) typed
observational equivalence of $t$ and $t'$.

\squelch{
\begin{figure*}[tph]
\iffull\[
\begin{array}{rcl}
\semV{x}\eta &=& \eta(x)\\
\semV{c}\eta &=& \semV{c}\\
\semV{(v_1,v_2)}\eta &=& (\semV{v_1}\eta,\semV{v_2}\eta)\\
\semV{v.i}\eta &=& d_i\ \mbox{if $i=1,2$, $\semV{v}\eta = (d_1,d_2)$}\\
\semV{\vfix{f}{x}t}\eta &=& \funn
{g^\dagger\,\eta}{\mbox{, where
  $g(\eta,u)=\lambda d.\semV{t}\eta[f{\mapsto}\funn{u},x{\mapsto}d]$}}
\end{array}
\]
\[
\begin{array}{rcll}
\semV{v}\eta\ \heap &=&(\heap,\semV{v}\eta)\\
\semV{\myif{v}{t_2}{t_3}}\eta\heap &=&
\semV{t_2}\eta\heap & \mbox{if
  $\semV{v}\eta =\intt z$, $z\neq 0$}\\
\semV{\myif{x}{t_2}{t_3}}\eta &=&
\semV{t_3}\eta\heap & \mbox{if $\semV{v}\eta=\intt 0$}
\\
\semV{\letin{x}{t_1}{t_2}}\eta\ \heap,\; &=&
\bot\mbox{, when $\semV{t_1}\eta\ \heap=\bot$}\\
\semV{\letin{x}{t_1}{t_2}}\eta\ \heap&=&
\semV{t_2}\eta[x{\mapsto}u]\ \heap_1
\mbox{when $\semV{t_1}\eta\ \heap=(\heap_1,u)$}
\\
\semV{\myread{v}}\eta\ \heap &=& (\heap,\heap(\ensuremath{\ell}\xspace))\mbox{, when
$\semV{v}\eta=\reff \ensuremath{\ell}\xspace$}\\
\semV{\assign{v_1}{v_2}}\eta\ \heap &=&
(\heap[\ensuremath{\ell}\xspace{\mapsto}\semV{v_2}\eta],\intt 0)\mbox{, if
$\semV{v_1}\eta=\reff
\ensuremath{\ell}\xspace$}\\
\semV{\myref{v}}\eta\ \heap &=& \textit{new}(\heap,\semV{v}\eta)\\
\semV{v}\eta &=&\intt 0\mbox{, otherwise}\\
\semV{t}\eta\ \heap&=& (\heap,\intt 0)\mbox{, otherwise}
\end{array}
\]
\else
\vspace{-7mm}
\[
\begin{array}{l}
\semV{x}\eta = \eta(x),
\semV{c}\eta = \semV{c},
\semV{(v_1,v_2)}\eta = (\semV{v_1}\eta,\semV{v_2}\eta),
\semV{v.i}\eta = d_i\ \mbox{if $i=1,2$, $\semV{v}\eta = (d_1,d_2)$}\\
\semV{\vfix{f}{x}t}\eta = \funn
{g^\dagger\,\eta}{\mbox{, where
  $g(\eta,u)=\lambda d.\semV{t}\eta[f{\mapsto}\funn{u},x{\mapsto}d]$}}
\end{array}
\]
\[
\begin{array}{l}
\semV{\myif{v}{t_2}{t_3}}\eta\heap =
\semV{t_2}\eta\heap\,   \mbox{if
  $\semV{v}\eta =\intt z$, $z\neq 0$},
\semV{\myif{x}{t_2}{t_3}}\eta =
\semV{t_3}\eta\heap\,  \mbox{if $\semV{v}\eta=\intt 0$}
\\
\semV{\letin{x}{t_1}{t_2}}\eta\ \heap,\; =
\bot\mbox{, when $\semV{t_1}\eta\ \heap=\bot$},
\semV{\letin{x}{t_1}{t_2}}\eta\ \heap=
\semV{t_2}\eta[x{\mapsto}u]\ \heap_1
\mbox{when $\semV{t_1}\eta\ \heap=(\heap_1,u)$},\\
\semV{\myread{v}}\eta\ \heap = (\heap,\heap(\ensuremath{\ell}\xspace))\mbox{, when
$\semV{v}\eta=\reff \ensuremath{\ell}\xspace$},
\semV{\assign{v_1}{v_2}}\eta\ \heap =
(\heap[\ensuremath{\ell}\xspace{\mapsto}\semV{v_2}\eta],\intt 0)\mbox{, if
$\semV{v_1}\eta=\reff
\ensuremath{\ell}\xspace$},\\
\semV{\myref{v}}\eta\ \heap = \textit{new}(\heap,\semV{v}\eta)
\semV{v}\eta\ \heap =(\heap,\semV{v}\eta),
\semV{v}\eta =\intt 0\mbox{, otherwise},
\semV{t}\eta\ \heap= (\heap,\intt 0)\mbox{, otherwise}
\end{array}
\]
\fi
\caption{Semantics of the untyped meta language \label{seme}}
\vspace{-8mm}
\end{figure*}
}

\begin{figure*}[tph]
\vspace{-3mm}
\[
\infer{\Gamma\vdash \underline{n} : \valty{\keywd{int}}}{}
\quad
\infer{\Gamma,x:\tau\vdash x : \valty{\tau}}{}
\quad
\infer{\Gamma\vdash v:\ety{\tau}{\emptyset}}{\Gamma\vdash v:\valty{\tau}}
\quad
\infer{\Gamma\vdash e:\ety{\tau}{\varepsilon_2}}{\Gamma\vdash
e:\ety{\tau}{\varepsilon_1} & \varepsilon_1
\subseteq  \varepsilon_2}
\quad
\infer{\Gamma\vdash v.i:\valty{\tau_i}}{\Gamma\vdash
v:\valty{\tau_1\times\tau_2}}
\]
\[
\infer{\Gamma\vdash v_1\ v_2 : \ety{\tau_2}{\varepsilon}}
{\Gamma\vdash v_1:\valty{\tau_1\effto{\varepsilon}\tau_2} & \Gamma\vdash
v_2:\valty{\tau_1}}
\quad
\infer{\Gamma \vdash \keywd{()} : \keywd{unit}}{}
\qquad
 \infer{\Gamma\vdash\myif{v}{e_1}{e_2} : \ety{\tau}{\varepsilon}}
{\Gamma\vdash v:\valty{\keywd{int}} &
    \Gamma\vdash e_1:\ety{\tau}{\varepsilon} &
    \Gamma\vdash e_2:\ety{\tau}{\varepsilon}}
\]
\[
\infer{\Gamma\vdash
(v_1,v_2):\valty{\tau_1\times\tau_2}}
{\Gamma\vdash v_1:\valty{\tau_1} &
\Gamma\vdash v_2:\valty{\tau_2}}
\quad
\infer{\Gamma\vdash \letin{x}{e_1}{e_2}:\ety{\tau_2}{\varepsilon}}
{\Gamma\vdash e_1:\ety{\tau_1}{\varepsilon} &
  \Gamma,x{:}\tau_1\vdash e_2:\ety{\tau_2}{\varepsilon}}
\qquad
\infer{\Gamma\vdash \vfix{f}{x}{e} : \valty{\tau_1\effto{\varepsilon} \tau_2}}
{\Gamma,f{:}\tau_1\effto\varepsilon \tau_2,x{:}\tau_1\vdash
e:\ety{\tau_2}{\varepsilon}}
\]
\caption{Core rules for effect typing\label{tyres}\label{efte}}
\vspace{-5mm}
\end{figure*}
\begin{figure*}[tph]
\vspace{-3mm}
\[
\infer{\Gamma\vdash t=t:\ety{\tau}{\varepsilon}}
{\Gamma\vdash t:\ety{\tau}{\varepsilon}}
\quad
\infer{\Gamma\vdash t'=t:\ety{\tau}{\varepsilon}}
{\Gamma\vdash t=t':\ety{\tau}{\varepsilon}}
\quad
\infer{\Gamma\vdash t=t'':\ety{\tau}{\varepsilon}}
{\Gamma\vdash t=t':\ety{\tau}{\varepsilon} & \Gamma\vdash
t'=t'':\ety{\tau}{\varepsilon}}
\quad
\infer{\Gamma\vdash v=v':\ety{\tau}{\emptyset}}
{\Gamma\vdash v=v':\valty{\tau}}
\]
\iffull \vspace{2pt} \fi
\[
\infer{\Gamma\vdash (v_1,v_2).i = v_i :\valty{\tau_i}}
{\Gamma\vdash v_1:\valty{\tau_1} & \Gamma\vdash
v_2:\valty{\tau_2}}
\quad
\infer{\Gamma\vdash
(\vfix{f}{x}{t})=(\vfix{f}{x}{t'}):\valty{\tau_1\effto\varepsilon
\tau_2}}
{\Gamma,f:\tau_1\effto\varepsilon \tau_2, x{:}\tau_1\vdash
t=t':\ety{\tau_2}{\varepsilon}}
\quad
\infer{\Gamma\vdash v=(v.1,v.2):\valty{\tau_1\times\tau_2}}
{\Gamma\vdash v:\valty{\tau_1\times\tau_2}}
\]
\iffull \vspace{2pt} \fi
\[
\infer{\Gamma\vdash\letin{x}{v}{t} = t[v/x] : \ety{\tau_2}{\varepsilon}}
{\Gamma\vdash v:\ety{\tau_1}{\varepsilon} & \Gamma,x:\tau_1\vdash
t:\ety{\tau_2}{\varepsilon}}
\quad
\infer{\Gamma\vdash (\vfix{f}{x}{t})\,v = t[v/x, (\vfix{f}{x}{t})/f]:
\ety{\tau_2}{\varepsilon}}
{\Gamma,f:\tau_1\effto\varepsilon \tau_2, x{:}\tau_1\vdash
t:\ety{\tau_2}{\varepsilon} & \Gamma\vdash v:\tau_1}
\]
\iffull \vspace{2pt} \fi
\[
\infer{\Gamma\vdash\letin{x}{(\letin{y}{t_1}{t_2})}{t_3} =
\letin{y}{t_1}{\letin{x}{t_2}{t_3}} : \ety{\tau_3}{\varepsilon}}
{\Gamma\vdash t_1:\ety{\tau_1}{\varepsilon} & \Gamma\vdash
t_2:\ety{\tau_2}{\varepsilon} & \Gamma,x:\tau_2,y:\tau_1\vdash
t_3:\ety{\tau_3}{\varepsilon}}
\]
\caption{Basic equational theory (extract)\label{eqth}}
\iffull
\else
\vspace{-2mm}
\fi
\end{figure*}
\subsection{Some example programs}\label{examples}

~\newline

\paragraph{Dummy allocation}
Define $\textit{dummy}$ as
$
\sem{\lambda f.\lambda x.\letin{d}{\myref{0}}{f\ x}},
$
so $\textit{dummy}(f)$ behaves like $f$ but makes an
allocation whose result is discarded.
We will be able to show that $\textit{dummy}(f)$ displays no more
abstract effects than $f$, so that whatever program transformation
$f$ can participate in, $\textit{dummy}(f)$ can as well.

\paragraph{Memoisation}
Let \textit{memo} be the memoizing functional
\iffull
\[
\begin{array}{l}\llbracket\lambda f.
\letin{x}{\myref{\underline{0}}}{
\letin{y}{\myref{f\ \underline{0}}}{}}\\
\quad \lambda a.\myif{\textit{eq}\ a\ \myread{x}}{\myread{y}}
{\letin{r}{f\ a}{\assign{x}{a};\assign{y}{r};r}}
\rrbracket
\end{array}\]
where $t_1;t_2=\letin{\_}{t_1}{t_2}$ is sequential composition and
$\textit{eq}$ is an integer equality constant.
\else

\(
\begin{array}{l}\llbracket\lambda f.
\letin{x}{\myref{\underline{0}}}{
\letin{y}{\myref{f\ \underline{0}}}{}}\\
\quad \lambda a.\myif{\textit{eq}\ a\ \myread{x}}{\myread{y}}
{\letin{r}{f\ a}{\assign{x}{a};\assign{y}{r};r}}
\rrbracket
\end{array}
\)

\noindent
where $t_1;t_2=\letin{\_}{t_1}{t_2}$ is sequential composition and
$\textit{eq}$ is an integer equality constant.
\fi
We can justify the typing
$\textit{memo}:(\textit{int}\effto{\emptyset}\textit{int})\effto{\emptyset}(\textit{int}\effto{\emptyset}\textit{int})$, saying that if $f$ is observationally pure, $\textit{memo}\, f$, is too, and so can
participate in any program equivalence relying
on purity. This was not justified by our previous
model~\cite{DBLP:conf/ppdp/BentonKBH07}.

\paragraph{Set factory}
The next, more complicated, example is a program that can
create and manipulate sets implemented as linked lists.

If $\ensuremath{\ell}\xspace\in\mathbb{L}$ and $\heap\in\ensuremath{\mathbb{H}}$ and $U$ is a finite set of
integers and $P$ is a finite subset of $\mathbb{L}$ define
$S(\ensuremath{\ell}\xspace,\heap,U,P)$ to mean that in $\heap$ location $\ensuremath{\ell}\xspace$ points to
a linked list of integer values occupying at most the locations in $P$
(the ``footprint'') and so that the set of these integer values is
$U$. So, for example, if $\heap(\ensuremath{\ell}\xspace)=\reff {\ensuremath{\ell}\xspace_1}$ and
$\heap(\ensuremath{\ell}\xspace_1)=(\intt 1,\reff{\ensuremath{\ell}\xspace_2})$ and $\heap(\ensuremath{\ell}\xspace_2)=(\intt
1,\intt 0)$ then $S(\ensuremath{\ell}\xspace,\heap,\{1\}, \{\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2\})$ holds.

For each location $\ensuremath{\ell}\xspace$ define functions $\textit{mem}_\ensuremath{\ell}\xspace$,
$\textit{add}_\ensuremath{\ell}\xspace$, $\textit{rem}_\ensuremath{\ell}\xspace$ so that
$\textit{mem}_\ensuremath{\ell}\xspace(\intt i)$ checks whether $i$ occurs in the list
pointed to by $\ensuremath{\ell}\xspace$, returning $\intt 1$ iff yes, and---for the fun
of it---removes all duplicates in that list and relocates some of its
nodes.  Thus, in particular, if $\textit{mem}_\ensuremath{\ell}\xspace(\intt
i)(\heap)=(\heap_1,v)$ then if $S(\ensuremath{\ell}\xspace,\heap,U,P)$ one has
$S(\ensuremath{\ell}\xspace,\heap_1,U,P')$ for some $P'$ where $P'\subseteq
P\cup(\dom{\heap_1}\setminus\dom{\heap})$ and $v=\intt 1$ iff $i\in
U$.

The function $\textit{add}_\ensuremath{\ell}\xspace$ adds its integer argument to the
set, and $\textit{rem}_\ensuremath{\ell}\xspace$ removes it, each possibly making
``optimizations'' similar to $\textit{mem}_\ensuremath{\ell}\xspace$.

Now consider a function $\textit{setfactory}$ returning upon each call
a fresh location $\ensuremath{\ell}\xspace$ and a the tuple of functions
$(\textit{mem}_\ensuremath{\ell}\xspace,\textit{add}_\ensuremath{\ell}\xspace,\textit{rem}_\ensuremath{\ell}\xspace)$.
We will be able to justify the following
 semantic typing for $\textit{setfactory}$:
\iffull
\[
\textit{setfactory} : \forall\ensuremath{\mathsf{r}}.
\ety{(\textit{int}\effto{\rEff\ensuremath{\mathsf{r}}}\textit{int})\times
(\textit{int}\effto{\wEff\ensuremath{\mathsf{r}}}\textit{unit})\times
(\textit{int}\effto{\wEff\ensuremath{\mathsf{r}}}\textit{unit})} {\aEff\ensuremath{\mathsf{r}}}
\]
which  expresses   that  $\textit{setfactory}()$  allocates   in  some
\else

\(
\textit{setfactory} : \forall\ensuremath{\mathsf{r}}.
\ety{(\textit{int}\effto{\rEff\ensuremath{\mathsf{r}}}\textit{int})\times
(\textit{int}\effto{\wEff\ensuremath{\mathsf{r}}}\textit{unit})\times
(\textit{int}\effto{\wEff\ensuremath{\mathsf{r}}}\textit{unit})} {\aEff\ensuremath{\mathsf{r}}}
\)

\noindent
which  expresses   that  $\textit{setfactory}()$  allocates   in  some
\fi
(possibly fresh) region $\ensuremath{\mathsf{r}}$ and returns operations that only read
$\ensuremath{\mathsf{r}}$ (the  first one)  or write  in $\ensuremath{\mathsf{r}}$ (the  second and
third one)  even though, physically, all three  functions read, write,
and allocate.

Thus, these functions can participate in corresponding
effect-dependent program equivalences, in particular, two successive
$\textit{mem}$ operations may be swapped and duplicated; identical
updates may even be contracted.
\iffull\footnote{We
could
also consider a more object-oriented variant that works with
a basic type $\textit{set}_\ensuremath{\mathsf{r}}$ accepted as argument by the
operations.}
\fi

\paragraph{Interleaved Dummy allocation}
Consider the following example, which looks similar to the Dummy example
above, but where the dummy allocation happens after a proper allocation:
\iffull
\[
\begin{array}{l}
 e_1 = \letin{p}{\myref{0}}\letin{d}{\myref{0}} e; !p ~\textrm{ and }~
 e_2 = \letin{p}{\myref{0}} e; !p.
\end{array}
\]
Here $d$ is not free in $e$, but $p$ may be free.
\else

\(
\hspace{-4mm}
\begin{array}{l}
 e_1 = \letin{p}{\myref{0}}\letin{d}{\myref{0}} e; !p ~\textrm{ and }~
 e_2 = \letin{p}{\myref{0}} e; !p.
\end{array}
\)

\noindent
Here $d$ is not free in $e$, but $p$ may be free.
\fi
This simple difference leads to many problems when
attempting to prove
their equivalence. We sketch them below to also motivate
our technical solution introduced formally in the following Sections.

As normally done the
evolution of the heaps can be formally captured by using Kripke models,
where, intuitively, a world contains the set of locations allocated by
programs.
Whenever there is an allocation,
we advance from the current world $\w$ to a world $\w_1$, which contains
some fresh locations. However, we do not have control over this
evolution. In our example, assume that the programs above
start at the same world $\w$. The allocation of the proper location,
$p$,
in $e_1$ and in $e_2$ will yield two different extensions $\w \to \w_1$ and
$\w \to \w_1'$, where some concrete locations, $\ensuremath{\ell}\xspace_1$ and $\ensuremath{\ell}\xspace_2$, are
allocated respectively. In fact, $\w_1$ and $\w_1'$ may even contain other
locations that are not used by the computations. For proving the
equivalence between these programs, we need
a way to capture that $\ensuremath{\ell}\xspace_1$  and $\ensuremath{\ell}\xspace_2$ are equivalent, without
requiring to identify the other locations not used by computations.

\begin{wrapfigure}{r}{.25\textwidth}
 \vspace{-12mm}
\begin{displaymath}
\vcenter{\xymatrix@C=1pc@R=0.5pc{
& \overline{\w}\\
\w_1\ar[ru]^x & & \w_1'\ar[lu]_{x'}\\
& \underline{\w}\ar[ru]_{u'} \ar[lu]^u
}}
\end{displaymath}
\caption{Pullback square.}
\label{fig:pullback}
\vspace{-9mm}
\end{wrapfigure}
Our solution is to use \emph{pullback squares} as proofs. Their shape is
depicted in Figure~\ref{fig:pullback}.
where $\underline{\w}$ and $\overline{\w}$ are called, respectively, the
\emph{low point} and \emph{apex} of the square.  It helps to interpret
$\overline{\w} $ as a superset of $\w_1 \cup \w_1'$, that is, a world
containing all the locations mentioned in $\w_1$ and $\w_1'$, even the
locations not used by computations, while $\underline{\w} = \w_1
\cap \w_2$ (modulo renaming of location names) is a world containing only
the locations that need to be identified. Intuitively, the low point
is the part of the proof showing that resulting heaps of computations are
equivalent. This is formalized by Definition~\ref{teffde}. In the
example above,
the low point is a world where $\ensuremath{\ell}\xspace_1$ and $\ensuremath{\ell}\xspace_2$ are
shown to be equivalent. The remaining locations in $\w_1$ and $\w_1'$ that
are not used by computations may be ignored, that is, not be contained in
$\underline{\w}$.
The apex, $\overline{\w}$, on the other hand, is the part of the proof
showing that the corresponding \emph{values} resulting from computations,
$!p$ in the example above, are indeed equivalent (see again
Definition~\ref{teffde}).

\section{Setoids}
\label{sec:setoids}
We define the \emph{category of setoids} as the exact completion of
the category of predomains, see
\cite{DBLP:conf/mfps/CarboniFS87,DBLP:conf/lics/BirkedalCRS98}. We
give here an elementary description using the language of dependent
types.  A \emph{setoid} $A$ consists of a predomain $|A|$ and for any
two $x,y\in |A|$ a set $A(x,y)$ of ``proofs'' (that $x$ and $y$ are
equal). The set of triples $\{(x,y,p) \mid p\in A(x,y)\}$ must itself
be a predomain and the first and second projections must be
continuous. Furthermore, there are continuous functions $r_A:\Pi x\in
|A|.A(x,x)$ and $s_A:\Pi x,y\in |A|.A(x,y)\rightarrow A(y,x)$ and
$t_A:\Pi x,y,z.A(x,y)\times A(y,z)\rightarrow A(x,z)$.
\iffull
We should explain what continuity of a dependent function like
$t(-,-)$ is: if $(x_i)_i$ and $(y_i)_i$ and $(z_i)_i$ are ascending
chains in $A$ with suprema $x,y,z$ and $p_i\in A(x_i,y_i)$ and $q_i\in
A(y_i,z_i)$ are proofs such that $(x_i,y_i,p_i)_i$ and $(y_i,z_i,q_i)_i$
are ascending chains, too, with suprema $(x,y,p)$ and $(y,z,q)$ then
$(x_i,z_i,t(p_i,q_i))$ is an ascending chain of proofs (by
monotonicity of $t(-,-)$) and its supremum is $(x,z,t(p,q))$.
\fi
\iffull
 Formally,
such dependent functions can be reduced to non-dependent ones using
pullbacks, that is $t$ would be a function defined on the pullback of
the second and first projections from $\{(x,y,p)\mid p\in A(x,y)\}$ to
$|A|$, but we find the dependent notation to be much more readable.
\fi
If $p\in A(x,y)$ we may write $p:x\sim y$ or simply $x\sim y$. We also
omit $|-|$ wherever appropriate. We remark that ``setoids'' also appear in
constructive mathematics and formal proof, see e.g.,
\cite{DBLP:journals/jfp/BartheCP03}, but the proof-relevant nature of
equality proofs is not exploited there and everything is based on sets
(types) rather than predomains.
A morphism from setoid $A$ to setoid $B$ is an equivalence class of  pairs $f=(f_0,f_1)$ of
continuous functions where $f_0:|A|\rightarrow |B|$ and $f_1:\Pi
x,y\in|A|.A(x,y)\rightarrow B(f_0(x),f_0(y))$. Two such pairs
$f,g:A\rightarrow B$ are \emph{identified} if there exists a
continuous function $\mu:\Pi a\in|A|.B(f(a),g(a))$.
\begin{proposition}
The category of setoids is cartesian closed; moreover, if $D$ is a setoid such that $|D|$ has a least element $\bot$ and there is also a least proof $\bot\in D(\bot,\bot)$ then there is a morphism of setoids $Y:[D\rightarrow D]\rightarrow D$ satisfying the usual fixpoint equations.
\end{proposition}
\subsection{Pullback squares}
\label{sec:pullback}
A morphism $u$ in a category $\ensuremath{\mathbf{W}}\xspace$ is a monomorphism if $ux=ux'$
implies $x=x'$ for all morphisms $x,x'$.  A commuting square $xu=x'u'$
of morphisms is a pullback if whenever $xv=x'v'$ there is unique $t$
such that $v=ut$ and $v'=u't$. We write $\sq{x}{u}{x'}{u'}$ or
$\w\sq{x}{u}{x'}{u'}\w'$ (when $\w^( {}' {}^)=\dom{x^( {}' {}^)}$) for such a
pullback square. We call the common codomain of $x$ and $x'$ the
\emph{apex} of the pullback written $\overline{\w}$, while
the common domain of $u,u'$ the \emph{low point} of the
square written $\underline{\w}$. A pullback square $xu=x'u'$ is
\emph{minimal} if
whenever $fx=gx$ and $fx'=gx'$ then $f=g$, in other words, $x$ and
$x'$ are \emph{jointly epic}. A pair of morphisms $u,u'$ with common domain
is a span, a pair of morphisms $x,x'$ with common codomain is a
co-span. A category has pullbacks if every co-span can be completed to
a pullback square.
\begin{definition}[Category of worlds]
  A category $\ensuremath{\mathbf{W}}\xspace$ is a \emph{category of worlds} if it has
  pullbacks and every span can be completed to a minimal pullback
  square and all morphisms are monomorphisms.
\end{definition}
\begin{example}
  The category of sets and injections is a category of worlds.
Given $f:X\to Z$ and $g:Y\to Z$, we form their pullback as
$X\xleftarrow{f^{-1}} fX\cap gY \xrightarrow{g^{-1}} Y$. This is minimal when $fX\cup gY = Z$. Conversely, given a span $Y\xleftarrow{f} X \xrightarrow{g}Z$, we can complete to a minimal pullback by
\newcommand{\myin}[1]{\mathit{in}_{#1}}
\iffull
\[
(Y\setminus fX) \uplus fX \xrightarrow{[\myin{1}, \myin{3}\circ f^{-1}]}
(Y\setminus fX) + (Z\setminus gX) + X
\xleftarrow{[\myin{2}, \myin{3}\circ g^{-1}]} (Z\setminus gX) \uplus gX
\]
where $[-,-]$ is case analysis on the disjoint union $Y = (Y\setminus
fX)\uplus fX$.
\else

\(
(Y\setminus fX) \uplus fX \xrightarrow{[\myin{1}, \myin{3}\circ f^{-1}]}
(Y\setminus fX) + (Z\setminus gX) + X
\xleftarrow{[\myin{2}, \myin{3}\circ g^{-1}]} (Z\setminus gX) \uplus gX
\)

\noindent
where $[-,-]$ is case analysis on the disjoint union $Y = (Y\setminus
fX)\uplus fX$.
\fi

  Given an arbitrary category $\mathbf{C}$, the
  category of worlds $\ensuremath{\mathbf{W}}\xspace_{\mathbf C}$ has objects pairs
  $(X,f)$ where $X$ is a set and $f:X\rightarrow |\mathbf{C}|$ is an
  $X$-indexed family of $\mathbf{C}$-objects. A morphism from $(X,f)$
  to $(Y,g)$ is an injective function $u:X\rightarrow Y$ and a family
  of isomorphisms $\phi_x:f(x)\simeq g(u(x))$. The first components of
  the pullbacks and minimal pullbacks are constructed as in the
  previous example.
\end{example}
\iffull
\begin{definition}
Let $\ensuremath{\mathbf{W}}\xspace$ be a category of worlds.  Two pullbacks
$\w\sq{x}{u}{x'}{u'}\w'$ and $\w\sq{y}{v}{y'}{v'}\w'$ are isomorphic
if there is an isomorphism $f$ between the two low points of the
squares so that $vf=u$ and $v'f=u'$, thus also $uf^{-1}=v$ and
$u'f^{-1}=v'$.
\end{definition}
\fi\iffull
\begin{lemma}\label{preo}
  Given a category of worlds $\ensuremath{\mathbf{W}}\xspace$, such that $\w, \w', \w'' \in
\ensuremath{\mathbf{W}}\xspace$,
  if $\w\sq{x}{u}{x'}{u'}\w'$ and $\w'\sq{y}{v}{y'}{v'}\w''$ are
  pullback squares as indicated then there exist $z,z',t,t'$ such that
  $\w\sq{zx}{ut}{z'y'}{v't'}\w''$ is also a pullback.
\end{lemma}
\fi
\iffull\begin{proof}
  Choose $z,z',t,t'$ in such a way that $\sq{z}{x'}{z'}{y}$ and
  $\sq{u'}{t}{v}{t'}$ are pullbacks.  The verifications are then an
  easy diagram chase.
\end{proof}
\fi

We write $r(\w)$ for $\w\sq{1}{1}{1}{1}\w$ and $s(\sq{x}{u}{x'}{u'}) =
\sq{x'}{u'}{x}{u}$ and $t(\sq{x}{u}{x'}{u'}, \sq{y}{v}{y'}{v'})=
\sq{zx}{z'y'}{ut}{v't'}$ where $z,z',t,t'$ \iffull are given by
Lemma~\ref{preo} assuming an arbitrary choice. \else are chosen so
that all four participating squares are pullbacks.\fi
\iffull
\begin{lemma}\label{decomp}
A pullback  square $\sq{x}{u}{x'}{u'}$ in a category of worlds is
isomorphic to $t(\sq{x}{1}{1}{x}, \sq{1}{x'}{x'}{1})$.
\end{lemma}
\fi

\subsection{Setoid-valued functors}
\label{subsec: func-setoids}
A functor $A$ from a category
of worlds $\ensuremath{\mathbf{W}}\xspace$ to the category of setoids comprises as usual for
each $\w\in \ensuremath{\mathbf{W}}\xspace$ a setoid $A\w$ and for each $u:\w\rightarrow \w'$
a morphism of setoids $Au:A\w\rightarrow A\w'$ preserving identities
and composition. If $u:\w\rightarrow \w'$ and $a\in A\w$ we may write
$u.a$ or even $ua$ for $Au(a)$ and likewise for proofs in $A\w$. Note
that $(uv).a=u.(v.a)$.

\begin{definition}
We call a functor
\emph{pullback-preserving} (p.p.f.) if for every pullback square
$\w\sq{x}{u}{x'}{u'}\w'$ with apex $\overline{\w}$ and low point
$\underline{\w}$ the diagram $A\w\sq{Ax}{Au}{Ax'}{Au'}A\w'$ is a pullback
in $\Std$. This means that there is a continuous function of type
\iffull
\[
\Pi a\in A\w.\Pi a'\in A\w'.A\overline{w}(x.a,x'.a')\rightarrow \Sigma
\underline{a}\in
A\underline{w}.A\w(u.\underline{a},a)\times
A\w'(u'.\underline{a},a')
\]
\else

\(
\Pi a\in A\w.\Pi a'\in A\w'.A\overline{w}(x.a,x'.a')\rightarrow \Sigma
\underline{a}\in
A\underline{w}.A\w(u.\underline{a},a)\times
A\w'(u'.\underline{a},a')
\)
\fi
\end{definition}
Thus, if two values $a\in A\w$ and $a'\in A\w'$ are equal in a common world
$\overline{\w}$ then this can only be the case because there is a value in
the ``intersection world'' $\underline{\w}$ from which both $a,a'$ arise.
Intuitively, p.p.f.s will become the denotations
of value types.
\iffull
\begin{lemma}
  If $A$ is a p.p.f., $u:\w\rightarrow \w'$ and $a,a'\in A\w$,
  there is a continuous function $A\w'(u.a,u.a')\rightarrow
  A\w(a,a')$. Moreover, the ``common ancestor'' $\underline{a}$ of $a$ and $a'$ is unique up to
$\sim$.
\end{lemma}
Note that the ordering on worlds and world morphisms is discrete so
that continuity only refers to the $A\w'(u.a,u.a')$ argument.
\fi
\iffull
\begin{definition}[Morphism of functors]\label{morphfun}
  If $A,B$ are p.p.f., a morphism from $A$ to $B$ is a pair
  $e=(e_0,e_1)$ of continuous functions where
  $e_0:\Pi\w.A\w\rightarrow B\w$ and $e_1:\Pi\w.\Pi\w'.\Pi
  x:\w\rightarrow\w'.\Pi a\in A\w.\Pi a'\in
  A\w'.A\w'(x.a,a')\rightarrow B\w'(x.e_0(a),e_0(a'))$. A proof that
  morphisms $e,e'$ are equal is given by a continuous function
  $\mu:\Pi \w.\Pi a\in A\w.B\w(e(a),e'(a))$.
\end{definition}
These morphisms compose in the obvious way and so
the faithful functors and morphisms between them form a category.
\fi
\subsection{Fibred setoids}\label{fibse} In order to provide
meanings for computation types we need a weaker variant of p.p.f.,
namely, \emph{fibred setoids}. These lack the facility of transporting
values along world morphisms but instead allow the proof-relevant
comparison of values at different worlds provided the latter are
related by a pullback square.
\begin{definition}
\label{def:fibred-setoids}
  A \emph{fibred setoid} over a category of
  worlds $\ensuremath{\mathbf{W}}\xspace$ is given by a predomain $T\w$ for every
  $\w\in\ensuremath{\mathbf{W}}\xspace$ and for every pullback square $\w\Diamond \w'$ and
  elements $a\in T\w$ and $a'\in T\w'$ a set $T\Diamond(a,a')$ so that
  the set of tuples $(a,a',q)$ with $q\in T\Diamond(a,a')$ is a
  predomain with continuous projections.

  Next, we need continuous operations $r,s,t$ so that $r(a)\in
  Tr(\w)(a,a)$ when $a\in T\w$ and $s(q)\in Ts(\Diamond)(a',a)$ when
  $q\in T\Diamond(a,a')$ and $t(q,q')\in Tt(\Diamond,\Diamond')(a,a'')$ when
  $q\in T\Diamond(a,a')$ and $q'\in T\Diamond'(a',a'')$.

  In addition, for any two isomorphic pullback squares $\Diamond$ and
  $\Diamond'$ between $\w$ and $\w'$ there is a continuous operation
  of type $\Pi a\in T\w.\Pi a'\in T\w'.T\sq(a,a')\rightarrow T\sq'(a,a')$.

  Finally, for each pullback square $\Diamond = \w\sq{x}{u}{x'}{u'}\w'$
  with apex $\overline{\w}$ and low point $\underline{\w}$ there is a
  continuous function of type
\iffull
\[
\Pi t\in T\w.\Pi t'\in T\w'.T\Diamond(t,t')\rightarrow \Sigma
\underline{t}\in T\underline{\w}.T\sq{u}{1}{1}{u}(\underline{t},t)\times
T\sq{u'}{1}{1}{u'}(\underline{t},t')
\]
\else

\(
\Pi t\in T\w.\Pi t'\in T\w'.T\Diamond(t,t')\rightarrow \Sigma
\underline{t}\in T\underline{\w}.T\sq{u}{1}{1}{u}(\underline{t},t)\times
T\sq{u'}{1}{1}{u'}(\underline{t},t')
\)
\fi
\end{definition}
Note the similarity of the last operation to pullback-preservation.

\begin{example}
  If $A$ is a p.p.f.,\  we obtain a fibred setoid $S(A)$ as follows:
  $S(A)\w=A\w$ and if $\w\sq{x}{u}{x'}{u'}\w'$ with apex $\overline \w$,
 define the proof set $S(A)
  \sq{x}{u}{x'}{u'}(a,a')=A\overline \w(x.a,x'.a')$.
\iffull If $\sq{x}{u}{x'}{u'}$ and
  $\sq{y}{v}{y'}{v'}$ are two composable pullback squares with
  composite $\sq{zx}{ut}{z'y'}{v't'}$ and $p\in S(A) \sq{x}{x'}{u}{u'}
  (a,a')$ and $p'\in S(A) \sq{y}{y'}{v}{v'} (a',a'')$, then the composite
proof of $t_{S(A)}(p,p')\in S(A)\sq{zx}{ut}{z'y'}{v't'}(a,a'')$ is given
by $t_A(z.p,z'.p')$. Indeed, if $\hat\w=\cod z$ is the apex of the
composite square  then  $z.p\in A{\hat\w}(zx.a,zx'.a')$ and $z'.p'\in
A{\hat\w}(z'y.a',z'y'.a'')$ and $zx'.a'=z'y.a'$ since $zx'=z'y$ so the
two proofs compose in $A{\hat \w}$.  \fi
\end{example}
\iffull
\begin{lemma}\label{baf}
  Let $T$ be a fibred setoid.  The elements $\underline{t}$ given by pullback
  preservation are unique up to $\sim$.  If $u:\w\rightarrow \w'$ is
  an isomorphism then there is a continuous function
  $Tu:T\w\rightarrow T\w'$ and it is bijective up to $\sim$ with
  inverse $T(u^{-1})$. If $\Diamond$ and $\Diamond'$ are isomorphic pullback squares then there are continuous back and forth functions
$\Pi t.\Pi t'.T\Diamond(t,t')\rightarrow T\Diamond'(t,t')$.
\end{lemma}
\fi
\begin{definition}
  A \emph{morphism} $f$ from fibred setoid $T$ to fibred setoid $T'$
  is an equivalence class  of pairs of continuous functions $f_0:\Pi \w.T\w\rightarrow T'\w$ and
  $f_1:\Pi \w,\w'.\Pi \w \Diamond\w'.\Pi a\in T\w.\Pi a'\in
  T\w'.T\Diamond(a,a') \rightarrow T'\Diamond(f_0(\w,a),f_0(\w',a'))$.

  Two such pairs  $f,f'$ are identified if there exists a continuous
function that assigns to each $\w$ and $a\in T\w$ a
proof $\mu(a)\in T{r(\w)}(f_0(\w,a),f_0'(\w,a))$.
\end{definition}
\ifful
\begin{lemma}\label{meanterm}
  If $A$ is a p.p.f.\ and $T$ is a fibred setoid then in
  order to specify a morphism from $S(A)$ to $T$ with given first
  component $f_0: \Pi\w.A\w\rightarrow T\w$ it is enough to provide a
  continuous function $f_{0.5}:\Pi\w,\w'.\Pi x:\w\rightarrow \w'.\Pi
  a\in A\w.\Pi a'\in A\w'.A\w'(x.a,a')\rightarrow
  T\sq{x}{1}{1}{x}(f_0(a),f_0(a'))$.
\end{lemma}
\begin{proof}
  If $(f_0,f_1)$ is a morphism we can define $f_{0.5}$ by
  $f_{0.5}(x,p)=f_1(x,a,a',p)$ noting that $p\in
  S(A)\sq{x}{1}{1}{x}(a,a')$.  Conversely, given $f_{0.5}$ to define
  $f_1$ we pick a pullback square $\w\sq{x}{u}{x'}{u'}\w'$ with apex
  $\overline{\w}$ and $a\in A\w, a'\in A\w'$ and $p\in A{\overline
    \w}(x.a,x'.a')$, i.e., a proof in $S(A){\Diamond}(a,a')$.  Applying
  $f_{0.5}$ to $r(-)$ yields the morphism $p_1\in
  T\sq{x}{1}{1}{x}(f_0(a),f_0(x.a))$; moreover, applying $f_{0.5}$ to
$s(p)$
  yields $p_2\in T\sq{x'}{1}{1}{x'}(f_0(a'),f_0(x.a))$.  Then,
  $t(p_1,s(p_2))\in
  Tt(\sq{x}{1}{1}{x},\sq{1}{x'}{x'}{1})(f_0(a),f_0(a'))$ so that
  Lemmas~\ref{decomp} and \ref{baf} yield the desired proof in the square
  $T\sq{x}{u}{x'}{u'}(f_0(a),f_0(a'))$.

  The second part of the lemma about equality is just a restatement of
  the definition of equality of morphisms of fibred setoids.
\end{proof}\fi
\iffull
\begin{lemma}
Let $A,B$ be p.p.f.\ For every morphism $e:A\rightarrow B$ there  is a
morphism $S(e):S(A)\rightarrow S(B)$ such that $S(e)_0=e_0$. Thus, in
particular $S(-)$ is a full and faithful functor from the category  of
p.p.f.\ on $\ensuremath{\mathbf{W}}\xspace$ to the category of fibred setoids over $\ensuremath{\mathbf{W}}\xspace$.
\end{lemma}
\fi
\subsection{Contravariant functors and relations} \label{reles} The
role of the next concept is to give meaning to abstract stores.
\begin{definition}
  A contravariant functor $\mathfrak{S}$ from a category of worlds
  $\ensuremath{\mathbf{W}}\xspace$ to the category of setoids comprises for each $\w\in
  \ensuremath{\mathbf{W}}\xspace$ a \emph{nonempty} setoid $\mathfrak{S} \w$ and for each morphism
  $u:\w_0\rightarrow \w$ a setoid morphism $\mathfrak{S} u:\mathfrak{S}
  \w\rightarrow \mathfrak{S} \w_0$ such that $u\mapsto \mathfrak{S} u$ preserves
  identities and composition.
\end{definition}
If $\sigma\in\mathfrak{S} \w$ and $u:\w_0\rightarrow \w$ we
  write $\sigma.u$ or $\sigma u$ for $\mathfrak{S} u(\sigma)$. Note that
  $\sigma.(uv)=(\sigma.u).v$. Intuitively, $\sigma.u$ can be interpreted
as the abstract heap obtained by forgetting locations in $\sigma$ that have
been ``allocated'' by the world evolution specified by $u$, namely, those
appearing in \w and not in $\w_0$.
\iffull
The following definition corresponds to the p.p.f. used for values, but
now for abstract heaps: In particular, an abstract heap at the
low-point of a pullback square is the result of forgetting locations from
an abstract heap at its
apex.
\fi
\begin{definition}
A contravariant functor $\mathfrak{S}$ preserves \emph{minimal pullbacks}
if whenever $\w\sq{x}{u}{x'}{u'}\w'$ with apex $\overline{\w}$ and low
point
$\underline{\w}$ is a \emph{minimal pullback square} then
the diagram $\mathfrak{S}\w\sq{\mathfrak{S} u}{\mathfrak{S} u'}{\mathfrak{S} x}{\mathfrak{S}
x'} \mathfrak{S} \w'$ is a pullback in $\Std$.
\end{definition}
This means in particular that if $\sigma\in
\mathfrak{S}\w, \sigma'\in \mathfrak{S}\w'$ and $\sigma.u\sim\sigma'.u'$
 then there exists a ``pasting''
$\overline{\sigma}\in \mathfrak{S}\overline{\w}$ such that
$\overline{\sigma}.x\sim \sigma$ and
$\overline{\sigma}.x'\sim\sigma'$ and $\overline{\sigma}$ is unique
up to $\sim$. Moreover the passage from the given data to
$\overline\sigma$ and the witnessing proofs is continuous.
\iffull
Application to the trivial minimal pullback $\sq{u}{1}{1}{u}$ and
nonemptiness yields the following result.
\begin{lemma}
\label{lem:unique-upto-sim}
   For every $u:\w\rightarrow \w'$ and $\sigma\in\mathfrak{S}\w$ there is
morphism of setoids $\mathfrak{S} \w\rightarrow \mathfrak{S} \w'$ which is right
inverse to $(-).u$.
\end{lemma}
The ``unique up to $\sim$'' clause allows us in particular to assert the $\sim$-equality of two abstract stores $\sigma,\sigma'\in\mathfrak{S}\overline{w}$ by proving $\sigma.x\sim\sigma'.x$ and $\sigma.x'\sim\sigma'.x'$ separately when $\sq{x}{u}{x'}{u'}$ is a minimal pullback  with apex $\overline{\w}$.
\fi
\begin{definition}
A \emph{relation} $R$ on such a contravariant functor $\mathfrak{S}$
consists of an admissible subset $R\w\subseteq \mathfrak{S} \w \times \mathfrak{S}
\w$ such that $(\sigma,\sigma')\in R \w$ and $u:\w_0\rightarrow \w$ implies
$(\sigma.u,\sigma'.u)\in R \w_0$ and if $p:\sigma\sim \sigma_1$ and
$p':\sigma'\sim\sigma_1'$ then $(\sigma_1,\sigma_1')\in R\w$, as well.
\end{definition}

It would be natural to let relations be proof-relevant as well, but we
refrain from doing so at this stage for the sake of simplicity.

\section{Computational model}
\label{test}
We use a setoid interpretation in order to justify
nontrivial type-dependent observational equivalences for the
language above. This interpretation is parametric over an
\emph{instantiation},
defined below.
\begin{definition}
An \emph{instantiation} comprises the following data.

\noindent \textbullet~a category of worlds $\ensuremath{\mathbf{W}}\xspace$;

\noindent \textbullet~a full-on-objects subcategory $\mathbf{I}$ of
\emph{inclusions}
  (in other words, a subset of the morphisms closed under composition
  and comprising the identities) with the property that every morphism
  $u$ can be factored as $u=fi$ and $u=jg$ with $f,g$ isomorphisms and
  $i,j$ inclusions;

\noindent \textbullet~a contravariant, minimal-pullback-preserving, functor $\mathfrak{S}$ from $\ensuremath{\mathbf{W}}\xspace$ to
the category of setoids;

\noindent \textbullet~for each $\w\in\ensuremath{\mathbf{W}}\xspace$ a relation
  $\Vdash_\w\subseteq\ensuremath{\mathbb{H}}\times \mathfrak{S} \w$ subject to the axiom
  that $\heap\Vdash_\w \sigma$ and $u\in\mathbf{I}(\w_0,\w)$ implies
  $\heap\Vdash_{\w_0}\sigma.u$;

\noindent \textbullet~a set of elementary effects $\mathcal{E}$ and for each
effect $\varepsilon$ a
set  $\Rscr(\varepsilon)$ of relations on $\mathfrak{S}$. As usual, one defines
effects as sets of elementary effects and extends $\Rscr$ to all
effects by $\Rscr(\emptyset)=$ ``all relations on $\mathfrak{S}$
 (in the sense described in Section~\ref{reles})'' and
$\Rscr(\varepsilon)=\bigcap_{\varepsilon_0\in\varepsilon}\Rscr(\varepsilon_0)$.
\end{definition}

We give \iffull three \else two \fi examples of instantiations.
\ifapp
The appendix
\else
The long version
\fi
contains a third example, mirroring our previous
model \cite{DBLP:conf/ppdp/BentonKBH09}.

\subsection{Sets of locations}
In the first one, called \emph{sets of locations}, worlds are finite
sets of (allocated) locations (taken from $\mathbb{L}$) and their morphisms
are injective functions with inclusions being actual
inclusions. Abstract stores are given by $\mathfrak{S} \w=\{\heap\mid
\dom\heap\supseteq\w\}$ with $\mathfrak{S}\w(\heap,\heap')=\star$, always,
and $\mathfrak{S} u$ given by renaming locations.

We put $\heap \Vdash_\w \heap'$ whenever $\heap=\heap'$.  We only have
one elementary effect here, $\aEff{}$, representing the allocation of
one or more fresh names. Note that if $R$ is a relation on $\mathfrak{S}$
then $R\w$ is either total or empty and if $u:\w\rightarrow\w'$ then
$R\w'\neq\emptyset\Rightarrow R\w\neq\emptyset$. A relation $R$ is in
$\mathcal{R}(\aEff{})$ if for every inclusion $u:\w\rightarrow\w'$ one
also has $R\w\neq\emptyset\Rightarrow R\w'\neq\emptyset$, thus $R$ is
oblivious to world extensions.

\iffull
\subsection{Flat stores}
The second instantiation, called \emph{flat stores}, assumes that heap
locations contain merely integer values and no pointers.
Possible worlds are
finite sets of locations together with a function that associates each
location a \emph{region} taken from a fixed set $\ensuremath{\mathit{Regs}}$ of
regions. World morphisms must preserve this tagging. We write
$\ensuremath{\ell}\xspace\in\w$ and $\ensuremath{\ell}\xspace\in\w(\ensuremath{\mathsf{r}})$ to mean that $\ensuremath{\ell}\xspace$ occurs in $\w$
and with region $\ensuremath{\mathsf{r}}$ in the second case.  Abstract stores
$\mathfrak{S} \w$ comprise those heaps $\heap\in\ensuremath{\mathbb{H}}$ with $\dom
\heap\supseteq
\w$ and such that $\ensuremath{\ell}\xspace\in\w$ and $\heap\in\mathfrak{S}\w$ implies that
$\heap(\ensuremath{\ell}\xspace)$ is an integer value, $\intt v$ for $v\in\mathbb{Z}$
 (thus all locations hold integer
values). We put $\heap\sim \heap'$ in $\mathfrak{S}\w$ iff for all $\ensuremath{\ell}\xspace\in
\w$
one has $\heap(\ensuremath{\ell}\xspace)=\heap'(\ensuremath{\ell}\xspace)$. In this case there is a unique proof,
say $\star$.  For morphism $u:\w\rightarrow \w'$ we define $\mathfrak{S}
u:\mathfrak{S} \w'\rightarrow \mathfrak{S} \w$ by renaming concrete locations
according to $u$. The elementary effects are $\rEff\ensuremath{\mathsf{r}},
\wEff\ensuremath{\mathsf{r}},\aEff\ensuremath{\mathsf{r}}$ representing reading from within, writing
into, allocating within a region $\ensuremath{\mathsf{r}}$. The associated sets of
relations are given by
\iffull
\[
 \begin{array}{lcl}
R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w \Rightarrow
\forall \ensuremath{\ell}\xspace\in \w(\ensuremath{\mathsf{r}}). \sigma(\ensuremath{\ell}\xspace)=\sigma'(\ensuremath{\ell}\xspace)
\\[3pt]

R\in\mathcal{R}(\wEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w \Rightarrow
\forall \ensuremath{\ell}\xspace\in \w(\ensuremath{\mathsf{r}}).\forall v\in\mathbb{Z}.\Rightarrow
(\sigma[\ensuremath{\ell}\xspace{\mapsto}\intt{v}],\sigma'[\ensuremath{\ell}\xspace{\mapsto}\intt{
v}])\in R\w
\\[3pt]

R\in\mathcal{R}(\aEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w
\Rightarrow \forall \w_1.\forall u\in\mathbf{I}(\w,\w_1). (\dom
{\w_1}\setminus \dom{\w} \subseteq \dom{\w_1(\ensuremath{\mathsf{r}})}) \\
&& \quad
\Rightarrow \forall \sigma_1\in \mathfrak{S} \w_1,\sigma_1'\in \mathfrak{S} \w_1'.
\sigma_1.u\sim \sigma\wedge \sigma_1'.u\sim\sigma'\wedge\\
&& \qquad \forall\ensuremath{\ell}\xspace\in
\dom{\w_1}\setminus\dom \w.  \sigma_1(\ensuremath{\ell}\xspace)=\sigma_1'(\ensuremath{\ell}\xspace) \Rightarrow
(\sigma_1,\sigma_1')\in R \w_1
 \end{array}
\]
This essentially models the setting of our earlier relation-based
\else

\(
\hspace{-5mm}
 \begin{array}{lcl}
R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w \Rightarrow
\forall \ensuremath{\ell}\xspace\in \w(\ensuremath{\mathsf{r}}). \sigma(\ensuremath{\ell}\xspace)=\sigma'(\ensuremath{\ell}\xspace)
\\[3pt]

R\in\mathcal{R}(\wEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w \Rightarrow
\forall \ensuremath{\ell}\xspace\in \w(\ensuremath{\mathsf{r}}).\forall v\in\mathbb{Z}.\Rightarrow
(\sigma[\ensuremath{\ell}\xspace{\mapsto}\intt{v}],\sigma'[\ensuremath{\ell}\xspace{\mapsto}\intt{
v}])\in R\w
\\[3pt]

R\in\mathcal{R}(\aEff{\ensuremath{\mathsf{r}}})&\iff& (\sigma,\sigma')\in R\w
\Rightarrow \forall \w_1.\forall u\in\mathbf{I}(\w,\w_1). (\dom
{\w_1}\setminus \dom{\w} \subseteq \dom{\w_1(\ensuremath{\mathsf{r}})}) \\
&& \quad
\Rightarrow \forall \sigma_1\in \mathfrak{S} \w_1,\sigma_1'\in \mathfrak{S} \w_1'.
\sigma_1.u\sim \sigma\wedge \sigma_1'.u\sim\sigma'\wedge\\
&& \qquad \forall\ensuremath{\ell}\xspace\in
\dom{\w_1}\setminus\dom \w.  \sigma_1(\ensuremath{\ell}\xspace)=\sigma_1'(\ensuremath{\ell}\xspace) \Rightarrow
(\sigma_1,\sigma_1')\in R \w_1
 \end{array}
\)

\noindent
This essentially models the setting of our earlier relation-based
\fi
account of reading, writing, and allocation with integer values stores
\cite{DBLP:conf/ppdp/BentonKBH09} the difference being that allocation
is modelled with relations on the same level as reading and writing
and that the stores being related share the same layout.
\fi

\subsection{Abstract locations}
To formulate the \iffull third \else second \fi instantiation, called
\emph{Heap PERs}, we need the concept of an \emph{abstract location}
which generalises physical locations in that it models a portion of
the store that can be read from and updated. Such portion may comprise
a fixed set of physical locations or a varying such set (as in the
case of a linked list with some given root). It may also reside in
just a part of a physical location, e.g., comprise the two low order
bits of an integer value stored in a physical location. Furthermore,
the equality on such abstract location may be coarser than physical
equality, e.g., two linked lists might be considered equal when they
hold the same set of elements, and there may be an invariant, e.g.\
the linked list should contain integer entries and be neither circular
nor aliased with other parts of the heap. This then prompts us to
model an abstract location as a partial equivalence relation (PER) on
heaps together with two more components that describe how
modifications of the abstract location interact with the heap as a
whole. Thus, next to a PER, an abstract location also contains a bunch
of (continuous) functions that model \emph{writing to the} abstract
location. These functions are closed under composition (thus form a
category) and are idempotent in the sense of the PER modelling
equality.

Thirdly, a ``footprint'' which is a heap-dependent set of
physical locations which overapproximates the effect of ``the
guarantee'' so as to enable the creation of fresh abstract locations
not knowing the precise nature of the other abstract locations that
are already there. (These footprints are very similar to
accessibility maps, first introduced for reasoning in a model of state based on FM-domains \cite{DBLP:conf/tlca/BentonL05}.)

\begin{definition}
\label{def:abstract-location}
  An \emph{abstract location} $\ensuremath{\mathsf{L}}\xspace$ (on the chosen predomain
  $\ensuremath{\mathbb{H}}$) consists of the following data:
\begin{compactitem}
\item a nonempty, admissible partial equivalence relation (PER) $\ensuremath{\mathsf{L}}\xspace^R$ on
  $\ensuremath{\mathbb{H}}$ modelling the ``semantic equality'' on the bits of the
  store that $\ensuremath{\mathsf{L}}\xspace$ uses (a ``rely-condition'');
\item a set $\ensuremath{\mathsf{L}}\xspace^G$ of continuous functions on $\ensuremath{\mathbb{H}}$ closed by
composition, modelling the functions that ``write only on $\ensuremath{\mathsf{L}}\xspace$'' leaving
other locations alone (a ``guarantee condition'');
\item a continuous function $\ensuremath{\mathsf{L}}\xspace^F:\Pi
  \heap\in\ensuremath{\mathbb{H}}.\mathcal{P}(\dom\heap)$ describing the ``footprint''
   of the abstract location (where the ordering on the powerset
$\mathcal{\dom\heap}$ is of course discrete).
\end{compactitem}
subject to the conditions
\begin{compactitem}
\item if $\iota\in \ensuremath{\mathsf{L}}\xspace^G$ and $(\heap,\heap')\in\ensuremath{\mathsf{L}}\xspace^R$ then $(\iota(\heap),\iota(\heap')),
(\iota(\heap),\iota(\iota(\heap))), (\iota(\heap'),\iota(\iota(\heap')))\in\ensuremath{\mathsf{L}}\xspace^R$,
\item if $\forall\ensuremath{\ell}\xspace\in\ensuremath{\mathsf{L}}\xspace^F(\heap).\heap_1(\ensuremath{\ell}\xspace)=\heap(\ensuremath{\ell}\xspace)$
  and $\forall\ensuremath{\ell}\xspace\in\ensuremath{\mathsf{L}}\xspace^F(\heap').\heap_1'(\ensuremath{\ell}\xspace)=\heap'(\ensuremath{\ell}\xspace)$
  then $(\heap,\heap')\in\ensuremath{\mathsf{L}}\xspace^R$ implies
  $(\heap_1,\heap_1')\in\ensuremath{\mathsf{L}}\xspace^R$; thus $\ensuremath{\mathsf{L}}\xspace^R$ ``looks'' no further
  than the footprint;
\item if $\iota \in \ensuremath{\mathsf{L}}\xspace^G$ and $\iota(\heap) = \heap_1$ then
  $\dom\heap\subseteq\dom{\heap_1}$ and
  $\ensuremath{\ell}\xspace\in\dom\heap\setminus \ensuremath{\mathsf{L}}\xspace^F(\heap)$ implies $\ensuremath{\ell}\xspace\not\in
  \ensuremath{\mathsf{L}}\xspace^F(\heap_1)$ and $\heap(\ensuremath{\ell}\xspace)=\heap_1(\ensuremath{\ell}\xspace)$.
\end{compactitem}
Two abstract locations $\ensuremath{\mathsf{L}}\xspace_1,\ensuremath{\mathsf{L}}\xspace_2$ are independent if
\begin{compactitem}
\item for $i=1,2$ and $\iota(\heap)=\heap_1$ for $\iota\in\ensuremath{\mathsf{L}}\xspace^G_i$ one has
$(\heap,\heap)\in\ensuremath{\mathsf{L}}\xspace_i^R, (\heap,\heap')\in\ensuremath{\mathsf{L}}\xspace_{3-i}^R\Rightarrow (\heap_1,\heap')\in\ensuremath{\mathsf{L}}\xspace_{3-i}^R$
and
$\ensuremath{\ell}\xspace\in\dom\heap\setminus\ensuremath{\mathsf{L}}\xspace_{3-i}^F(\heap)$
then $\ensuremath{\ell}\xspace\notin\ensuremath{\mathsf{L}}\xspace_{3-i}^F(\heap_1)$;
\item If $(\heap_1,\heap_1)\in\ensuremath{\mathsf{L}}\xspace_1^R$ and $(\heap_2,\heap_2)\in\ensuremath{\mathsf{L}}\xspace_2^R$
there exists $\heap$ such that $(\heap,\heap_1)\in\ensuremath{\mathsf{L}}\xspace_1^R$ and
$(\heap,\heap_2)\in\ensuremath{\mathsf{L}}\xspace_2^R$. (Amounting to
$\heap/(\ensuremath{\mathsf{L}}\xspace_1^R\cap\ensuremath{\mathsf{L}}\xspace_2^R)$ being a cartesian product of $\heap/\ensuremath{\mathsf{L}}\xspace_1^R$ and $\heap/\ensuremath{\mathsf{L}}\xspace_2^R$.)
\end{compactitem}
If $\ensuremath{\mathsf{L}}\xspace_1, \ensuremath{\mathsf{L}}\xspace_2$ are independent, we form a joint location
$\ensuremath{\mathsf{L}}\xspace_1\otimes\ensuremath{\mathsf{L}}\xspace_2$ by $(\ensuremath{\mathsf{L}}\xspace_1\otimes\ensuremath{\mathsf{L}}\xspace_2)^R=\ensuremath{\mathsf{L}}\xspace_1^R\cap\ensuremath{\mathsf{L}}\xspace_2^R$
and
$(\ensuremath{\mathsf{L}}\xspace_1\otimes\ensuremath{\mathsf{L}}\xspace_2)^G=(\ensuremath{\mathsf{L}}\xspace_1^G\cup\ensuremath{\mathsf{L}}\xspace_2^G)^*$ and
$(\ensuremath{\mathsf{L}}\xspace_1\otimes\ensuremath{\mathsf{L}}\xspace_2)^F(\heap)=\ensuremath{\mathsf{L}}\xspace_1^F(\heap)\cup\ensuremath{\mathsf{L}}\xspace_2^F(\heap)$.

\end{definition}

If $\ensuremath{\ell}\xspace\in\ensuremath{\labs}$ is a concrete location, we can define an abstract
counterpart by putting $\ensuremath{\ell}\xspace^R=\{(\heap,\heap')\mid
\heap(\ensuremath{\ell}\xspace)=\heap'(\ensuremath{\ell}\xspace)\}$ and $\ensuremath{\ell}\xspace^G$ is the set with a
write function for each value that may be stored in $\ensuremath{\ell}\xspace$.
For instance, if $\ensuremath{\ell}\xspace$ stores booleans, then $\ensuremath{\ell}\xspace^G$ contains the
functions $write_\keywd{true}$ and $write_\keywd{false}$, where
$write_\keywd{true}(\heap) = \heap'$ such that $\heap'(\ensuremath{\ell}\xspace) =
\keywd{true}$ and
for all other locations $\ensuremath{\ell}\xspace' \neq \ensuremath{\ell}\xspace$, $\heap'(\ensuremath{\ell}\xspace') =
\heap(\ensuremath{\ell}\xspace')$.
When $\ensuremath{\ell}\xspace_1 \neq \ensuremath{\ell}\xspace_2$ then the induced abstract locations are
independent.

The next example illustrates that abstract locations may be
independent although their footprints share some concrete locations.
Fix a concrete location $\ensuremath{\ell}\xspace$ and define two abstract
locations $\ensuremath{\mathsf{L}}\xspace_1$ and $\ensuremath{\mathsf{L}}\xspace_2$ both with footprint consisting of the
location $\ensuremath{\ell}\xspace$. Moreover, $(\heap, \heap')$ belong, respectively, to
the rely of location $\ensuremath{\mathsf{L}}\xspace_i$ ($i=1,2$) if $\heap(\ensuremath{\ell}\xspace)$ and
$\heap'(\ensuremath{\ell}\xspace)$ are both integers whose $i$-th significant bit
agrees. The ``guarantee'' $\ensuremath{\mathsf{L}}\xspace_i^G$ might then contain functions that
set the $i$-th bit to some fixed value and leave the other bits
alone. It is easy to see that $\ensuremath{\mathsf{L}}\xspace_1,\ensuremath{\mathsf{L}}\xspace_2$ are independent.

Thirdly, let $\ensuremath{\ell}\xspace_1, \ensuremath{\ell}\xspace_2$ be two distinct concrete locations and
for heap $\heap$ and finite integer sets $U_1,U_2$ define
$P(\heap,U_1,U_2)$ to mean that in $\heap$ the locations $\ensuremath{\ell}\xspace_1,
\ensuremath{\ell}\xspace_2$ point to non-overlapping integer lists with \emph{sets} of
elements $U_1$ and $U_2$. Now define abstract location $\ensuremath{\mathsf{L}}\xspace_i$ by
$\ensuremath{\mathsf{L}}\xspace_i^R= \{(\heap,\heap')\mid \exists
U_1,U_2.P(\heap,U_1,U_2)\wedge P(\heap',U_1,U_2)\}$
 and $\ensuremath{\mathsf{L}}\xspace_i^F(\heap)=$ ``locations reachable from
$\ensuremath{\ell}\xspace_i$'' if $\ensuremath{\ell}\xspace$ points to a well-formed list of integers in
$\heap$ and $\emptyset$ otherwise. The guarantee component $\ensuremath{\mathsf{L}}\xspace_i^G$
contains all the (idempotent) functions $\iota$ that leave the locations
not in the footprint of $\ensuremath{\mathsf{L}}\xspace_i$ alone. That $\iota(\heap) = \heap'$,
such that $\heap'(\ensuremath{\ell}\xspace') = \heap(\ensuremath{\ell}\xspace')$ for all $\ensuremath{\ell}\xspace' \in
\dom{\heap}\setminus \ensuremath{\mathsf{L}}\xspace_i^F$.
Again, $\ensuremath{\mathsf{L}}\xspace_1$ and $\ensuremath{\mathsf{L}}\xspace_2$ are independent.

The role of the footprints $\ensuremath{\mathsf{L}}\xspace^F$ is to provide a minimum amount of
interaction with physical allocation. If $\ensuremath{\mathsf{L}}\xspace$ is an abstract
location and $\heap_0$ the current heap so that
$(\heap_0,\heap_0)\in\ensuremath{\mathsf{L}}\xspace^R$ then we may, e.g., allocate
$(\heap_1,\ensuremath{\ell}\xspace)=\ensuremath{\mathit{new}}(\heap_0,\intt 0)$, and define an abstract location
$\ensuremath{\mathsf{L}}\xspace_1$ by

\(
 \begin{array}{lcl}
\ensuremath{\mathsf{L}}\xspace_1^R&=&\{(\heap,\heap')\mid
\heap(\ensuremath{\ell}\xspace)=\heap'(\ensuremath{\ell}\xspace)\in\intt{\mathbb{Z}}\wedge
\ensuremath{\ell}\xspace\not\in\ensuremath{\mathsf{L}}\xspace^F(\heap)\wedge \ensuremath{\ell}\xspace\not\in\ensuremath{\mathsf{L}}\xspace^F(\heap')\}\\
\ensuremath{\mathsf{L}}\xspace_1^G&=&\{\iota\mid \iota(\heap) = \heap_1 \Rightarrow \forall
\ensuremath{\ell}\xspace'\neq\ensuremath{\ell}\xspace.\heap(\ensuremath{\ell}\xspace')=\heap_1(\ensuremath{\ell}\xspace')\}\\
\ensuremath{\mathsf{L}}\xspace_1^F(\heap)&=&\{\ensuremath{\ell}\xspace\}
 \end{array}
\)

\noindent
We now know that $\ensuremath{\mathsf{L}}\xspace$ and $\ensuremath{\mathsf{L}}\xspace_1$ are independent and, furthermore,
$(\heap_1,\heap_1)\in(\ensuremath{\mathsf{L}}\xspace\otimes\ensuremath{\mathsf{L}}\xspace_1)^R$.
\begin{definition}
Abstract  locations $\ensuremath{\mathsf{L}}\xspace_1,\dots,\ensuremath{\mathsf{L}}\xspace_n$ are mutually independent if they are pairwise independent and whenever $(\heap_i,\heap_i)\in\ensuremath{\mathsf{L}}\xspace_i$ for $i=1\dots n$ then there is $\heap$ such that $(\heap_i,\heap)\in\ensuremath{\mathsf{L}}\xspace_i$ for $i=1\dots n$.
\end{definition}
\begin{lemma}
Abstract locations $\ensuremath{\mathsf{L}}\xspace_1,\dots,\ensuremath{\mathsf{L}}\xspace_{n+1}$ are mutually independent iff $\ensuremath{\mathsf{L}}\xspace_1,\dots,\ensuremath{\mathsf{L}}\xspace_n$ are mutually independent and $\ensuremath{\mathsf{L}}\xspace_{n+1}$ is independent of $\ensuremath{\mathsf{L}}\xspace_1\otimes\dots\otimes\ensuremath{\mathsf{L}}\xspace_n$.
\end{lemma}
\subsection{Heap PERs}
We are now ready to formulate the \iffull third \else second \fi
instantiation \emph{Heap
  PERs}. We assume an infinite set of \emph{regions} $\ensuremath{\mathit{Regs}}$. A
world $\w$ comprises a finite set of mutually independent abstract
locations (written $\w$) and as in the case of flat stores a tagging of
locations with regions from $\ensuremath{\mathit{Regs}}$
location. We write $\ensuremath{\mathsf{L}}\xspace\in \w(\ensuremath{\mathsf{r}})$ to mean that $\ensuremath{\mathsf{L}}\xspace\in\w$
is tagged with $\ensuremath{\mathsf{r}}$. We define $\mathfrak{S} \w =
\{\heap\in\ensuremath{\mathbb{H}}\mid \forall \ensuremath{\mathsf{L}}\xspace\in\w.(\heap,\heap)\in\ensuremath{\mathsf{L}}\xspace^R\}$ and
$\mathfrak{S} \w(\sigma,\sigma')=\{\star\}\iff \forall \ensuremath{\mathsf{L}}\xspace\in\w.
(\sigma,\sigma')\in\ensuremath{\mathsf{L}}\xspace^R$ and $\mathfrak{S}
\w(\sigma,\sigma')=\emptyset$ otherwise. Again, $\heap\Vdash_\w \sigma$
iff $\heap=\sigma$.

A morphism from $\w$ to $\w'$ is given by an injective function $u_0:
\w\rightarrow \w'$ and a pair of partial continuous functions
$u_1,u_2:\ensuremath{\mathbb{H}}\rightharpoondown\ensuremath{\mathbb{H}}$. Intuitively, the function $u_1$
is used
to map the heaps in the PERs of locations in $\w$ to $\w'$ according to the
renaming of locations specified in $u_0$, while $u_2$
does the same but from $\w'$ to $\w$. Formally,
$\forall \sigma,\sigma'\in\mathfrak{S} \w.  \forall
\ensuremath{\mathsf{L}}\xspace\in\w.(\sigma,\sigma')\in\ensuremath{\mathsf{L}}\xspace^R\Rightarrow
(u_1(\sigma),u_1(\sigma'))\in u_0(\ensuremath{\mathsf{L}}\xspace)^R \wedge
(u_2(u_1(\sigma)),\sigma)\in\ensuremath{\mathsf{L}}\xspace^R$ and $\forall
\sigma,\sigma'\in\mathfrak{S} \w'.  \forall
\ensuremath{\mathsf{L}}\xspace\in\w.(\sigma,\sigma')\in u_0(\ensuremath{\mathsf{L}}\xspace)^R \Rightarrow
(u_2(\sigma),u_2(\sigma'))\in \ensuremath{\mathsf{L}}\xspace^R \wedge
(u_1(u_2(\sigma)),\sigma)\in u_0(\ensuremath{\mathsf{L}}\xspace)^R$. The same is valid for
guarantees of locations, by replacing $\cdot^R$ by $\cdot^G$.
Now, $\mathfrak{S}
u(\sigma) = u_2(\sigma)$.  Such a morphism $u$ is an inclusion if
$u_0$ is an inclusion and $u_1,u_2$ are the identity function.

The elementary effects track reading, writing, and allocating at the
level of regions: $\wEff \ensuremath{\mathsf{r}}$ (writing within
region $\ensuremath{\mathsf{r}}$), $\rEff\ensuremath{\mathsf{r}}$ (reading from within region $\ensuremath{\mathsf{r}}$),
$\aEff\ensuremath{\mathsf{r}}$ (allocating within region $\ensuremath{\mathsf{r}}$).
The sets of relations on $\mathfrak{S}$ modelling elementary effects are then
given by
\iffull
\[
 \begin{array}{lll}
R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})& \iff &
(\sigma,\sigma')\in R\w \Rightarrow \forall \ensuremath{\mathsf{L}}\xspace\in\w(\ensuremath{\mathsf{r}}).
(\sigma,\sigma')\in\ensuremath{\mathsf{L}}\xspace^R\\[2pt]

R\in\mathcal{R}(\wEff{\ensuremath{\mathsf{r}}})&\iff&
(\sigma,\sigma')\in R\w \Rightarrow \forall \ensuremath{\mathsf{L}}\xspace\in\w(\ensuremath{\mathsf{r}}).\forall
\iota \in \ensuremath{\mathsf{L}}\xspace^G. (\iota(\heap), \iota(\heap')) \in R\w\\[2pt]

R\in\mathcal{R}(\aEff{\ensuremath{\mathsf{r}}})& \iff &
(\sigma,\sigma')\in R\w \Rightarrow \forall \w_1.\forall
u\in\mathbf{I}(\w,\w_1).(\w_1\setminus \w \subseteq
\w_1(\ensuremath{\mathsf{r}}))\Rightarrow \forall
\sigma_1,\sigma_1' \in\mathfrak{S}\w_1.\\
&& (\sigma_1.u\sim\sigma \wedge
\sigma_1'.u\sim\sigma'\wedge(\sigma_1,\sigma_1')\in \bigcap_{\ensuremath{\mathsf{L}}\xspace\in
\w_1\setminus \w}
\ensuremath{\mathsf{L}}\xspace^R)\Rightarrow (\sigma_1,\sigma_1')\in R\w_1
 \end{array}
\]
Thus, a relation $R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})$ ensures that
\else

\(
\hspace{-5mm}
 \begin{array}{lll}
R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})& \iff &
(\sigma,\sigma')\in R\w \Rightarrow \forall \ensuremath{\mathsf{L}}\xspace\in\w(\ensuremath{\mathsf{r}}).
(\sigma,\sigma')\in\ensuremath{\mathsf{L}}\xspace^R\\[2pt]

R\in\mathcal{R}(\wEff{\ensuremath{\mathsf{r}}})&\iff&
(\sigma,\sigma')\in R\w \Rightarrow \forall \ensuremath{\mathsf{L}}\xspace\in\w(\ensuremath{\mathsf{r}}).\forall
\iota \in \ensuremath{\mathsf{L}}\xspace^G. (\iota(\heap), \iota(\heap')) \in R\w\\[2pt]

R\in\mathcal{R}(\aEff{\ensuremath{\mathsf{r}}})& \iff &
(\sigma,\sigma')\in R\w \Rightarrow \forall \w_1.\forall
u\in\mathbf{I}(\w,\w_1).(\w_1\setminus \w \subseteq
\w_1(\ensuremath{\mathsf{r}}))\Rightarrow \forall
\sigma_1,\sigma_1' \in\mathfrak{S}\w_1.\\
&& (\sigma_1.u\sim\sigma \wedge
\sigma_1'.u\sim\sigma'\wedge(\sigma_1,\sigma_1')\in \bigcap_{\ensuremath{\mathsf{L}}\xspace\in
\w_1\setminus \w}
\ensuremath{\mathsf{L}}\xspace^R)\Rightarrow (\sigma_1,\sigma_1')\in R\w_1
 \end{array}
\)

\noindent
Thus, a relation $R\in\mathcal{R}(\rEff{\ensuremath{\mathsf{r}}})$ ensures that
\fi
locations being read contain ``equal'' (in the sense of $\ensuremath{\mathsf{L}}\xspace^R$)
values; a relation $R\in\mathcal{R}(\wEff{\ensuremath{\mathsf{r}}})$ is oblivious to
writes to any abstract location in $\ensuremath{\mathsf{r}}$, and a relation
$R\in\mathcal{R}(\aEff{\ensuremath{\mathsf{r}}})$ is oblivious to extensions of the
current world provided that it only adds abstract locations in region
$\ensuremath{\mathsf{r}}$, that the initial contents of these newly allocated locations
are ``equal'' in the sense of $(-)^R$ and that nothing else is
changed.

\section{Proof-relevant Logical Relations}
\label{sec:logical-relations}
Given an instantiation, e.g.\ one of the above examples, we
interpret types (and typing contexts) as p.p.f.\ over
$\ensuremath{\mathbf{W}}\xspace$ and types with effect as a fibred setoid over $S(\ensuremath{\mathbf{W}}\xspace)$. A
term in context $\Gamma\vdash e:\ety{\tau}{\varepsilon}$ will be interpreted as a
morphism $\sem{e}$ from $S(\sem{\Gamma})$ to $T_\varepsilon\sem{\tau}$ where
$T_\varepsilon$ takes p.p.f.\ and effects to fibred setoids and is
given below in Definition~\ref{teffde}. Derivations of equations
will be interpreted as equality proofs between the corresponding morphisms
and can be used to deduce observational equivalences
(Theorem~\ref{obseq}).

This, however, requires a loose relationship of the setoid interpretation
with the actual meanings of raw terms which is given by realization
relations $\Vdash^A$. Their precise format and role are described in the
following two  definitions.
\begin{definition}\label{defte}
  A \emph{semantic type} is a pair $(A,\Vdash^A)$ where $A$ is a
  p.p.f.\ (on $\ensuremath{\mathbf{W}}\xspace$) and $\Vdash^A_\w$ is an admissible
  subset of $\mathbb{V}\times A\w$ for each $\w\in \ensuremath{\mathbf{W}}\xspace$ such that for
  every inclusion $u:\w\rightarrow \w'$ one has that $\vval\Vdash^A_\w
  \val$ implies $\vval\Vdash^A_{\w'} u.\val$.  A \emph{semantic
computation} is a pair $(T,\Vdash^T)$ where $T$ is
  a fibred setoid over $\ensuremath{\mathbf{W}}\xspace$ and $\Vdash_\w^T$ is an
  admissible subset of $\mathbb{C}\times T\w$ for each $\w$.
\end{definition}
\begin{definition}
  Let $(\Gamma,\Vdash^\Gamma)$ and $(A,\Vdash^A)$ be semantic types
  and let $(T,\Vdash^T)$ be a semantic computation.  If
  $e:S(\Gamma)\rightarrow T$ is a morphism of fibred setoids and
  $f:\mathbb{V}\rightarrow \mathbb{C}$ then we write $f\Vdash^{\Gamma\vdash
    T}e$ to mean that for some representative $(f_0,f_1)$ of $f$ one has that
 whenever $\eta\Vdash^\Gamma_\w \gamma$ then
  $f_0(\eta)\Vdash^T_\w e(\gamma)$ holds for all worlds $\w$.

\end{definition}

The following definition, corresponding to that in Fig.~\ref{fig:oldklr}, is where the machinery introduced above pays off.
In particular, it defines the semantics of computations, where proofs,
i.e., pullback squares, are constructed.

\begin{definition}\label{teffde}\label{def:semantic-computation}
  Let $A$ be a semantic type and $\varepsilon$ an effect. A semantic
  computation $T_\varepsilon A$ is defined as follows:

\smallskip
\noindent \textbullet~ (Objects) Elements of $(T_\varepsilon A)\w$ are pairs
$(\cval_0,\cval_1)$ of partial continuous functions where
\iffull
\[
 \begin{array}{ll}
  \cval_0 : & \mathfrak{S} \w\rightharpoondown \Sigma
  \w_1.\mathbf{I}(\w,\w_1)\times \mathfrak{S} \w_1\times A\w_1
\end{array}
\]
and $\cval_1$ is as follows.  If $R\in \Rscr(\varepsilon)$ and
\else

\(
 \begin{array}{ll}
  \cval_0 : & \mathfrak{S} \w\rightharpoondown \Sigma
  \w_1.\mathbf{I}(\w,\w_1)\times \mathfrak{S} \w_1\times A\w_1
\end{array}
\)

\noindent
and $\cval_1$ is as follows.  If $R\in \Rscr(\varepsilon)$ and
\fi
$(\sigma,\sigma')\in R\w$ then $\cval_1(R,\sigma,\sigma')$ either is
undefined and $\cval_0(\sigma)$ and $\cval_0(\sigma')$ are both
undefined or else $c_1(R,\sigma,\sigma')$ is defined and then
$\cval_0(\sigma)$ and $\cval_0'(\sigma')$ are both defined, say
$\cval_0(\sigma)=(\w_1,u,\sigma_1,a)$ and
$\cval_0(\sigma')=(\w_1',u',\sigma_1',a')$. In this case,
$\cval_1(R,\sigma,\sigma')$ returns a pair $(\sq{x}{v}{x'}{v'},p)$
where $\w_1\sq{x}{v}{x'}{v'}\w_1'$ such that $xu=x'u'$.  Furthermore, $p\in
A \overline w (x.a,x'.a')$ and,
finally, $(\sigma_1.u,\sigma_1'.u')\in R \underline{\w}$ where
$\underline\w$ and $\overline\w$ are low point and apex of
$\sq{x}{v}{x'}{v'}$.

\smallskip
\noindent \textbullet~ (Proofs) As usual, proofs only look at the $(-)_0$
components.
  Thus, if $(\cval_0,\_)\in T_\varepsilon A \w$ and $(\cval_0',\_)\in T_\varepsilon
  A \w'$ and $\sq{x}{v}{x'}{v'}$ is in $S(\ensuremath{\mathbf{W}}\xspace)(\w,\w')$ with apex
  and low point $\overline\w, \underline\w$ then a proof in $(T_\varepsilon A)
  \sq{x}{v}{x'}{v'}(\cval,\cval')$ is a partial continuous function
  $\mu$ which given $\sigma\in\mathfrak{S} \w$ and $\sigma'\in\mathfrak{S}
  \w'$ and $p:\sigma.v\sim \sigma'.v'$ either is undefined and then
  $\cval_0(\sigma)$ and $\cval_0'(\sigma')$ are both undefined or else
  is defined and then $\cval_0(\sigma)$ and $\cval_0'(\sigma')$ are
  both defined with results, say,
  $\cval_0(\sigma)=(\w_1,u,\sigma_1,\val)$ and
  $\cval_0'(\sigma')=(\w_1',u',\sigma_1',\val')$. In this case,
  $\mu(p)$ returns a tuple $(\sq{x_1}{v_1}{x_1'}{v_1'},q)$ satisfying
  $x_1uv=x_1'u'v'$ and $q\in A{\overline{\w_1}}(x_1.\val,x_1'.\val')$
  with $\overline {\w_1} = \cod{x_1}$ and $\sigma_1.v_1\sim \sigma_1.v_1'$
  in $\mathfrak{S}{\underline {\w_1}}$.

\smallskip
\noindent \textbullet~ (Realization)
  If $c\in \mathbb{C}$, we define $\ccval\Vdash^{T_\varepsilon A}_\w
(\cval_0,\cval_1)$ to mean that
  whenever  $\heap\Vdash_\w \sigma$ then $\ccval(\heap)$ is defined iff
$\cval_0(\sigma)$ is defined and if $\ccval(\heap)=(\heap_1,\vval)$ and
$\cval_0(\sigma)=(\w_1,u,\sigma_1,\val)$ then
$\heap_1\Vdash_{\w_1}\sigma_1$ and $\vval\Vdash^A_{\w_1} \val$.
\end{definition}
\iffull
\begin{proposition}
The semantic computation $T_\varepsilon A$ as defined in
Definition~\ref{def:semantic-computation} is a fibred setoid.
\end{proposition}
\begin{proof}
  The tricky case is to show the existence of a transitive operation.
  It is here that we require the independence of abstract locations as
  stated in Definition~\ref{def:abstract-location}, which implies that
  $\mathfrak{S}$ is also minimal-pullback-preserving.

Assume that there are proofs in $p_1 : T_\varepsilon A \sq{x_1}{v_1}{x_1'}{v_1'}
(\cval, \cval')$ and $p_2 : T_\varepsilon A \sq{x_2}{v_2}{x_2'}{v_2'} (\cval',
\cval'')$ where
$\w \sq{x_1}{v_1}{x_1'}{v_1'} \w'$ and $\w' \sq{x_2}{v_2}{x_2'}{v_2'}
\w''$. We also have $\sigma \in \mathfrak{S} \w$ and $\sigma'' \in \mathfrak{S}
\w''$, such that they are equivalent in the pullback of
the low points of these two pullback squares. Let $\underline{\q}$ be such
pullback.

In order to use the proofs $p_1$ and $p_2$, we need to construct
from $\sigma$ and $\sigma''$ an abstract heap $\sigma' \in \mathfrak{S}\w'$.
Let $\overline{\q}$ be the minimal pullback over the apexes of the two pullback
squares $\w \sq{x_1}{v_1}{x_1'}{v_1'} \w'$ and $\w'
\sq{x_2}{v_2}{x_2'}{v_2'} \w''$. Then $\w$ and $\w''$ form a pullback
square with apex $\overline{\q}$ and low point $\underline{\q}$. Since
$\mathfrak{S}$ is minimal-pullback-preserving, there is a $\sigma_{\q} \in \mathfrak{S}
\overline{\q}$, such that it is equivalent to $\sigma$ and $\sigma''$ when
taken to the world $\underline{\q}$. We now define $\sigma' \in \mathfrak{S}
\w'$ to be $\sigma_{\q}$ taken to the world $\w'$. We thus have $\sigma'
\in \mathfrak{S}
\w'$, and $\sigma'' \in \mathfrak{S} \w''$, such that $\sigma.v_1 \sim
\sigma'.v_1'$ and $\sigma'.v_2' \sim \sigma''.v_2'$.

We can now use the $p_1$ and $p_2$. In particular,
let $\cval(\sigma) = (\w_1, u_1, \sigma_1, \val_1)$, $\cval'(\sigma') =
(\w_1', u_1', \sigma_1', \val_1')$, and $\cval''(\sigma'') = (\w_1'',
u_1'', \sigma_1'', \val_1'')$. From the proofs, we get two
pullback squares $\w_1\sq{}{}{}{}\w_1'$ and $\w_1'\sq{}{}{}{}\w_1''$. It
is easy to show that the values obtained are equal in the minimal pullback over
the
apexes of these two pullback squares and that the abstract heaps are
equivalent in the pullback of their low points.
\end{proof}
\else
Proving that a semantic computation $T_\varepsilon A$ as  in
Definition~\ref{def:semantic-computation} is a fibred setoid is
nontrivial.  The tricky case is the existence of a transitivity
 operation.
It is here that we need the independence of abstract locations as
stated in Definition~\ref{def:abstract-location}, which implies that
$\mathfrak{S}$ is also minimal-pullback-preserving.
\fi
\iffull
\begin{definition}[cartesian product]
If $(A,\Vdash^A)$ and $(B,\Vdash^B)$ are semantic types their cartesian product $(A\times B,\Vdash^{A\times B})$ is defined by $(A\times B)\w=A\w\times B\w$ (cartesian product of setoids) and $(v_1,v_2)\Vdash_\w^{A\times B}(a,b)\iff v_1\Vdash_\w^{A}a\wedge v_2\Vdash_\w^{B}b$.
\end{definition}
\begin{definition}[function space]
  Let $(A,\Vdash^A)$ be a semantic type and $(T,\Vdash^T)$ be a
  semantic computation. We define a semantic type $(A{\Rightarrow}T,
  \Vdash^{A{\Rightarrow}T})$ as follows.
  An object $f$ of $(A{\Rightarrow} T)\w$ is a pair $(f_0,f_1)$ of
  continuous functions where $f_0$ assigns to each $\w_1$ and
  $v:\w\rightarrow \w_1$ a continuous function $f_0(v):A\w_1\rightarrow
  T\w_1$. The second component $f_1$ assigns to each
  $v:\w\rightarrow \w_1$ and $v_1:\w_1\rightarrow \w_2$ a continuous
  function $\Pi a\in A\w_1.\Pi a'\in A\w_2.A\w_2(v_1.a,a')\rightarrow
  T\sq{v_1}{1}{1}{v_1}(f_0(v,a),f_0(v_1v,a'))$.

  If $f,f'\in |A{\Rightarrow}T|$ then a proof $\mu\in
  (A{\Rightarrow}T)(f,f')$ is a continuous function assigning to each
  $v:\w\rightarrow \w_1$ and $a\in A\w_1$ a proof $\mu(v,a)\in
  T\sq{1}{1}{1}{1}(f_0(v,a), f_0'(v,a))$.

  If $u:\w\rightarrow \w'$ and $f=(f_0,f_1)\in (A{\Rightarrow}T)\w$
  then $u.f\in (A{\Rightarrow}T)\w'$ is given by precomposition with
  $u$, i.e., $(u.f)_0(v,a)=f_0(vu,a)$, etc.

  As for the realisation relation $\Vdash^{A{\Rightarrow}T}$ we put
  $v\Vdash^{A{\Rightarrow}T}_\w f$ to mean that $v=\funn g$ for some
  $g$ and whenever $i:\w\rightarrow \w_1$ is an inclusion and
  $u\Vdash^A_{\w_1}a$ then $g(u)\Vdash^T_{\w_1} f(i,a)$.
\end{definition}
Notice that unlike morphisms the elements of the function space are \emph{not} identified if they are ``provably equal.''.
Notice also that if $v\Vdash^{A{\Rightarrow} T}_\w f$ implies
$v\Vdash^{A{\Rightarrow}T}_{\w_1}i.f$ whenever $i:\w\rightarrow \w_1$
is an inclusion.
\else
Details, along with the construction of the cartesian product
$(A\times B,\Vdash^{A\times B})$ and function space
 $(A{\Rightarrow}T, \Vdash^{A{\Rightarrow}T})$, given semantic types
 $(A,\Vdash^A)$ and $(B,\Vdash^B)$ and computation $(T,\Vdash^T)$,
may be found in the
\ifapp
appendix.
\else
long version of the paper.
\fi
\fi
\subsection{Fundamental theorem}
Given a semantic type $\sem{A}$ for each basic type
$A$ we can interpret any type $\tau$ as a semantic type $\sem{\tau}$
by putting
$\sem{\tau_1\effto\varepsilon\tau_2}=\sem{\tau_1}{\Rightarrow}T_\varepsilon\sem{\tau_2}
$. A
typing context $\Gamma=x_1{:}\tau_1,\dots,x_n{:}\tau_n$ is interpreted
as the semantic type
$\sem{\Gamma}=(1\times\sem{\tau_1})\times\dots)\times\sem{\tau_n}$
where $1$ is the constant functor returning the discrete setoid
$\{()\}$.

To every typing derivation $\Gamma\vdash t:\ety{\tau}{\varepsilon}$ we then
associate a morphism
$
\sem{\Gamma\vdash t:\ety{\tau}{\varepsilon}}:S(\sem{\Gamma})\rightarrow
T_\varepsilon\sem{\tau}
$
such that $\sem{t}\Vdash^{\sem{\Gamma}\rightarrow
T_\varepsilon\tau}\sem{\Gamma\vdash t:\ety{\tau}{\varepsilon}}$.
(Note: \emph{this} is point where the untyped semantics is related with the
abstract one.)
For every equality derivation $\Gamma\vdash t=t':\ety{\tau}{\varepsilon}$ we
have $\sem{\Gamma\vdash
t:\ety{\tau}{\varepsilon}} =
\sem{\Gamma\vdash t':\ety{\tau}{\varepsilon}}
$,
where the two typing derivations $\Gamma\vdash t:\ety{\tau}{\varepsilon}$ and
$\Gamma\vdash t':\ety{\tau}{\varepsilon}$ are the canonical ones associated with
the equality derivation $\Gamma\vdash t=t':\ety{\tau}{\varepsilon}$.
\iffull
In what follows we define semantic counterparts to the generic
syntactic constructions common to all instantiations, namely
application and abstraction, sequential composition, and recursion
that allow us to define this interpretation of derivations in a
compositional fashion. Having given these semantic counterparts we
then omit the formal definition of the interpretation $\sem{-}$.
\begin{lemma}[Abstraction]
Let $\Gamma,A$ be  semantic types, $T$ a semantic computation. There is a function $\lambda$ so that if $e:S(\Gamma\times A)\rightarrow T$ is a morphism of fibred setoids then $\lambda(e):S(\Gamma)\rightarrow A{\Rightarrow}T$. Moreover, if $e\sim e'$ then $\lambda(e)\sim\lambda(e')$ and if $f\Vdash^{\Gamma\times A\rightarrow T} e$ then $\lambda\eta.\lambda a.f(\eta,a)\Vdash^{\Gamma\rightarrow A{\Rightarrow}T} \lambda(e)$.
\end{lemma}
\begin{lemma}[Application]
Let $A$ be a semantic type and $T$ be a semantic computation. There  is a
morphism $\textit{app} : S((A{\Rightarrow}T)\times A)\rightarrow T$ and
$\lambda (f,a).f(a)\Vdash^{((A{\Rightarrow}T)\times A)\rightarrow T}
\textit{app}$.
\end{lemma}
We elide assertions about $\sim$-versions of beta-eta-equality, and semantic
rendering of subeffecting and the existence of ``value morphisms'' of type $S(A)\rightarrow T_\varepsilon A$ for any semantic type $A$.

\begin{lemma}[let]
Let $\Gamma,A,B$ be semantic types and $\varepsilon$ an effect.
There is a function $\textit{let}$ such that if $e_1:S(\Gamma)\rightarrow
T_\varepsilon A$ and $e_2:S(\Gamma\times A)\rightarrow T_\varepsilon B$ are morphisms
then $\textit{let}(e_1,e_2):S(\Gamma)\rightarrow T_\varepsilon B$. Moreover, if
$e_1\sim
e_1'$ and $e_2\sim e_2'$ then $\textit{let}(e_1,e_2)\sim
\textit{let}(e_1',e_2')$.
Finally, if $f_1\Vdash^{\Gamma\rightarrow T_\varepsilon A} e_1$ and
$f_2\Vdash^{\Gamma\times A\rightarrow T_\varepsilon B} e_2$ then $\lambda \eta.
\lambda \heap.\textit{let } (\heap_1,\vval){=}f_1(\eta)(\heap)\textit{ in }
f_2(\eta,\vval)(\heap_1)\Vdash^{\Gamma\rightarrow T_\varepsilon
A}\textit{let}(e_1,e_2)$.
\end{lemma}

\begin{proof}
Consider the following definition for the first component of the morphism
$\textit{let}(e_1,e_2)$ which is only defined when ${e_1}$ and
${e_2}$ are defined. The type of this component is $\sem{\Gamma}\w \to
T_\varepsilon \sem{B}\w$. Hence, assume a world $\w$, and a context $\gamma \in
\sem{\Gamma}\w$, then one returns an object $(\cval_0, \cval_1) \in
T_\varepsilon \sem{B}\w$. The first component $\cval_0$ is:
\(
 \Pi \w. \Pi \gamma \in \sem{\Gamma}\w . \Pi \sigma \in \mathfrak{S} \w.
{e_2}(\w_1)(\gamma,\val_1)\sigma_1
\)
where ${e_1}(\w)(\gamma)\sigma = (\w_1, u_1, \sigma_1, \val_1)$.

For the second component, $\cval_1$, assume a relation $R \in
\Rscr(\varepsilon)$, and two abstract heaps $\sigma, \sigma' \in \mathfrak{S} \w$
such that $(\sigma, \sigma') \in R\w$. From ${e_1}$ we get a
proof $\w_1 \sq{x_1}{v_1}{x_1'}{v_1'} \w_1'$, where
${e_1}(\w)(\gamma)\sigma
=
(\w_1, u_1, \sigma_1, \val_1)$ and ${e_1}(\w)(\gamma)\sigma' =
(\w_1', u_1', \sigma_1', \val_1')$, such that $(\sigma_1.v_1,
\sigma_1'.v_1') \in R$ and $p : \sem{A}\overline{\w_1}(x_1.\val_1,
x_1'.\val_1')$. Applying ${e_2}$ on $\sigma_1.v_1$ and
$\sigma_1'.v_1'$ we get a proof $\q_2 \sq{y_2}{v_2}{y_2'}{v_2'} \q_2'$,
such that $(\tilde{\sigma_2}.v_2, \tilde{\sigma_2}'.v_2') \in R$. However,
we need to show that the heaps obtained from applying ${e_2}$ on $\sigma_1$
and $\sigma_1'$ (using the correct world and context), namely $\sigma_2$
and $\sigma_2'$, are related. For this we rely on
the morphism $(e_2)_1$. In particular,
we use $(e_2)_1$ on the pullback $\w_1 \sq{1}{x_1}{x_1}{1} \und{\w_1}$ and
obtain a pullback $\w_2 \sq{}{}{}{} \q_2$ such that $\sigma_2$ and
$\tilde{\sigma_2}$
are equal in its low point. Similarly, applying $(e_2)_1$ on the
pullback $\und{\w_1} \sq{x_1'}{1}{1}{x_1'} \w_1'$, we get a pullback
$\q_2' \sq{}{}{}{} \w_2'$, where $\tilde{\sigma_2}'$ is equal to
$\sigma_2'$ in its pullback. Using Lemma~\ref{preo}, we compose the
pullbacks $\w_2 \sq{}{}{}{} \q_2$, $\q_2 \sq{}{}{}{} \q_2'$ and $\q_2'
\sq{}{}{}{} \w_2'$, obtaining a common pullback $\und{\q}$, where
$\sigma_2$ and $\sigma_2'$ when taken to $\und{\q}$ are in $R$.

The morphism ${\textit{let}(e_1,e_2)\sim
\textit{let}(e_1',e_2')}$ can be then defined when ${e_1 \sim e_1'}$
and ${e_2 \sim e_2'}$ are defined.
Assume a pullback $\w \sq{1}{1}{1}{1}\w$ and an abstract heap $\sigma \in
\mathfrak{S} \w$ and a context $\gamma \in \sem{\Gamma}\w$. Using the
morphism between $e_1$ and $e_1'$ on these objects, we obtain a
pullback $\w_1 \sq{x_1}{v_1}{x_1'}{v_1'} \w_1'$, $p_1 \in
\sem{A}\overline{\w_1}(x_1.\val_1, x_1'.\val_1')$ and $q_1 : \sigma_1.v_1
\sim \sigma_1'.v_1'$, where ${e_1}(\w)(\gamma)\sigma = (\w_1, u_1,
\sigma_1,
\val_1)$ and ${e_1'}(\w)(\gamma)\sigma = (\w_1', u_1', \sigma_1',
\val_1')$.
From the pullback preserving property of computations and $p_1$,
there is a common value $\und{\val} \in \sem{A}\und{\w_1}$ and context
$\und{\gamma} \in \sem{\Gamma}\und{\w_1}$ which are equal, respectively, to
$\val_1$ and $\val_1'$, and $\gamma$ and $\gamma'$ (when taken to the
correct world). We then construct a
proof $\sem{\Gamma \times A} \und{\w_1}$. We now apply twice the
morphism between $e_2$ and $e_2'$ once in the pullback $\w_1 \sq{}{}{}{}
\und{\w_1}$ and
another on the
pullback $\und{\w_1} \sq{}{}{}{} \w_1'$, obtaining two pullbacks
$\w_2 \sq{}{}{}{} \q_2$ and $\q_2 \sq{}{}{}{} \w_2'$. From
Lemma~\ref{preo}, we can compose them where the resulting values and
heaps are equal.
\end{proof}
\begin{lemma}[fix]\label{fixlse}
  Let $\Gamma,D$ be semantic types so that for each $\w$ the predomain
  $D\w$ is a domain with least element $\bot\w$ such that
  $(\bot\w,\bot\w,r(\bot\w))\leq (d,d',p)$ holds for every proof $p\in
  D(d,d')$ and such that $x.\bot_\w=\bot_{\w'}$ holds for every
  $x:\w\rightarrow\w'$.\footnote{For example $D=A {\Rightarrow}T_\varepsilon B$
for semantic types $A,B$.}
\begin{compactenum}
\item[i] There then exists a function
  $\textit{fix}$ so that whenever $e:\Gamma\times D\rightarrow D$ then
  $\textit{fix}(e):\Gamma\rightarrow
  D$
\item[ii] If $e\sim e'$ then $\textit{fix}(e)\sim
  \textit{fix}(e')$. Furthermore, the fixpoint and unrolling equations
  from Lemma~\ref{fixlse} hold.
\item[iii] Finally, if $f\Vdash^{\Gamma\times D\rightarrow D}e$ then
$f^\dagger\Vdash \textit{fix}(e)$.
\end{compactenum}
\end{lemma}
\begin{proof}
{\bf MH: dagger notation and accompanying lemma have disappeared}
For every $\w$ we have $e_0\w:\Gamma\w\times D\w
\rightarrow D\w$. We can thus form $\textit{fix}(e)_0\w:=(e_0\w)^\dagger :
\Gamma \w\rightarrow D\w$.  It remains to define $\textit{fix}(e)_1$. To do that, we
recall that we
have an ascending chain of elements
$\textit{fix}^n(e)_0\w(\gamma)\in D\w$ given by
$\textit{fix}^0(e)_0\w(\gamma)=\bot_\w$ and
$\textit{fix}^{n+1}(e)_0\w(\gamma)=e_0\w(\gamma,\textit{fix}
^n(e)_0\w(\gamma))$ and have
$\textit{fix}(e)_0\w(\gamma)=\sup_n\textit{fix}^n(e)_0\w\gamma$.
Now suppose that $\gamma\in\Gamma\w$ and $x:\w\rightarrow \w'$ and
$\gamma'\in\Gamma\w'$ and $p\in\Gamma\w'(x.\gamma,\gamma')$. Write
$d_n=\textit{fix}^n_0\w(\gamma)$ and $d_n'=\textit{fix}^n_0\w'(\gamma')$.
Inductively, we get proofs $p_n\in
D\w'(x.d_n,d_n')$ where $p_0=r(\bot_{\w'})$ (note that
$x.\bot_\w=\bot_{\w'}$) and $p_{n+1}=e_1(p,p_n)$. Since
$(x.\bot_\w,\bot_{\w'},r(\bot_{\w'}))\leq (x.d_1,d_1',p_1)$ we obtain by
monotonicity of $e_1$ and induction that $(x.d_n,d_n',p_n)$ is an ascending
chain with supremum $(x.\sup_n d_n,\sup_n d_n',q)$ for some proof $q$
which we take as $\textit{fix}(e)_1(p)$. Note that the passage from $p$ to
$q$ is continuous.
\end{proof}
\else
In essence, one has to provide a semantic counterpart for every
syntactic concept, e.g. let, fix, etc. Details are in the
\ifapp
appendix.
\else
long
version.
\fi
\fi

\subsection{Observational equivalence}
Let $\textrm{Int}$ stand for the constant functor that returns the
discrete setoid on the set $\mathbb{Z}$ of integers. We define
$v\Vdash^{\mathrm{Int}}_\w i\iff v=\intt i$. We also assume that there
is some initial store and abstract store $\heap_0, \sigma_0$ and a
world $\w_0$ such that $\heap_0\Vdash_{\w_0}\sigma_0$. For instance,
$\w_0$ can be the empty world with no locations and accordingly
$\heap_0$ the initial store at startup.

\begin{definition}
  Let $(A,\Vdash^A)$ be a semantic type.  We define an
  \emph{observation of type $A$} as a morphism $o:A\rightarrow T_\varepsilon
  \mathrm{Int}$ for some $\varepsilon$ and a function $f$ so that
  $f\Vdash^{A\rightarrow T_\varepsilon\mathrm{Int}}o$.

  Two values $v,v'$ are \emph{observationally equivalent at type $A$}
  if for all observations $f,o$ of type $A$ one has that $f(v)(\heap_0)$ is
  defined iff $f(v')(\heap_0)$ is defined and when
  $f(v)(\heap_0)=(\heap_1,v_1)$ and $f(v')(\heap_0)=(\heap_1',v_1')$
  then $v_1=v_1'$.
\end{definition}
Taking $o=\sem{\vdash f:\tau\effto\varepsilon\keywd{int}}$ immediately yields the following:
\begin{proposition}
If $v,v'$ are observationally equivalent at type $\sem{\tau}$ and $f$ is a
term such that $\vdash f:\tau\effto\varepsilon\keywd{int}$ then $\sem{f}(v)(\heap_0)$
is
  defined iff $\sem{f}(v')(\heap_0)$ is defined and when
  $\sem{f}(v)(\heap_0)=(\heap_1,v_1)$ and
$\sem{f}(v')(\heap_0)=(\heap_1',v_1')$
  then $v_1=v_1'$.
\end{proposition}
\begin{theorem}[Observational equivalence]
\label{thm:obs-equivalence}\label{obseq}
If $(A,\Vdash^A)$ is a semantic type and $v\Vdash^A_{\w_0}e$ and
$v'\Vdash^A_{\w_0}e'$ with $e\sim e'$ in $A_{\w_0}$ then $v$ and  $v'$ are
observationally equivalent at type $A$.
\end{theorem}
\begin{proof}
  We have $f(v)\Vdash^{T_\varepsilon \mathrm{Int}}_{\w_0} o(e)$ and $f(v')\Vdash^{T_\varepsilon \mathrm{Int}}_{\w_0} o(e')$ and also $\mu:
o(e)\sim_{\sq{1}{1}{1}{1}} o(e')$ in $T_\varepsilon\mathrm{Int}$ for some $\mu$ as in Definition~\ref{teffde}.

The application $\mu$ to $\sigma_0,\sigma_0,r(\sigma_0)$ either is
undefined in which case $o(e)(\sigma_0)$ and $o(e')(\sigma_0)$ and
$f(v)(\heap_0)$ and $f(v')(\heap_0)$ are all undefined, the latter by
the definition of $\Vdash^{T_\varepsilon \mathrm{Int}}$. Otherwise, we get
$f(v)(\heap_0)=(\heap_1,v_1)$ and $f(v')(\heap_0)=(\heap_1',v_1')$ and
$o(e)(\sigma_0)=(\sigma_1,i_1)$ and $o(e')(\sigma_0)=(\sigma_1',i_1')$
where, by definition of realization in $T_\varepsilon\mathrm{Int}$ and
$\mathrm{Int}$, we have $v_1=\intt{i_1}$ and $v_2=\intt{i_2}$. Now,
$\mu(\sigma_0,\sigma_0,r(\sigma_0))$ returns a pullback
$(\sq{x_1}{v_1}{x_1'}{v_1'},q)$ such that, in particular, $x_1.i_1\sim
x_2.i_2$, whence $i_1=i_2$ since $\mathrm{Int}$ is constant and then
$v_1=v_2$ as required.
\end{proof}

\section{Applications}
\label{sec:application}
In what follows we use our semantics to establish a number of
effect-dependent semantic equalities, hence program equivalences in
the sense of observational equivalences. We also give some
semantically justified typings of concretely given functions, in
particular ``set factory'' described in Section~\ref{examples}.
More examples are discussed in the
\ifapp
appendix.
\else
longer version of this paper.
\fi

\subsection{Sets of locations}
We work in the instantiation ``sets of locations''.  Recall the
example, ``dummy allocation'' from Section~\ref{examples}.  Suppose
that $f\Vdash^{\Gamma\vdash T_\varepsilon A} e$. Now, put
$\textit{dummy}(e)(\w)(\gamma \in \sem{\Gamma}\w) (\heap \in \mathfrak{S} \w)
= e(\w)(\gamma)(\heap')$, where $\heap'$ is the heap
obtained by adding a dummy location to \heap. We have
$\textit{dummy}(f)\Vdash^{\Gamma\vdash
  T_\varepsilon A} \textit{dummy}(e)$ since $\Vdash$ is oblivious to
extensions of the store. Therefore, reflexivity also furnishes a proof
of equality. It also means that, semantically, $\textit{dummy}(f)$
does not need to flag the allocation effect $\aEff{}$ since no
semantically visible world extension takes place.

For the Interleaved Dummy Allocation example, on the other hand, there is
an extra step caused by the proper allocation, which yields a world
extension $\w \to \w_1$ and $\w
\to \w_1'$. In order to show the equivalence, we construct a
proof, i.e., a pull-back square $\w_1\sq{}{}{}{}\w_1'$, where the
allocated concrete locations are identified in its low point. Then the
reasoning is the same as above used for showing the semantic equivalence
of the Dummy example.

This is different in the following example. Define a semantic type $N$
of names by letting $N\w$ be the discrete setoid on the set $\w$ and
$Nu(\ensuremath{\ell}\xspace)=u(\ensuremath{\ell}\xspace)$ and $v\Vdash_\w^N\ensuremath{\ell}\xspace\iff v=\reff\ensuremath{\ell}\xspace$.
\iffull
\(
 \begin{array}{ll}
f ~=~\sem{\myref{0}}\\
g ~=~ \sem{\letin{x}{\myref{0}}{\letin{y}{\myref{0}}{
(x,y)}}}\\
h ~=~ \sem{\letin{x}{\myref{0}}{\letin{y}{\myref{0}}{
(y,x)}}}
 \end{array}
\)

\noindent
We now define semantic counterparts $\textsf{f}:S(1)\rightarrow
T_{\aEff{}}N$,
$\textsf{g}, \textsf{h}:S(1)\rightarrow T_{\aEff{}}N$. We omit the dummy
arguments of type $1$.
\else
Moreover,
$f =\sem{\myref{0}},
g = \sem{\letin{x}{\myref{0}}{\letin{y}{\myref{0}}{
(x,y)}}}$, and $
h = \sem{\letin{x}{\myref{0}}{\letin{y}{\myref{0}}{
(y,x)}}}$.
We now define semantic counterparts $\textsf{f}:S(1)\rightarrow
T_{\aEff{}}N$,
$\textsf{g}, \textsf{h}:S(1)\rightarrow T_{\aEff{}}N$, where
\fi
\iffull
\[
 \begin{array}{lcl}
\textsf{f}_0\w(\sigma) & = & (\w_1,i_1,\sigma_1,\ensuremath{\ell}\xspace_1), \\
\textsf{g}_0\w(\sigma) & = & (\w_2,i_2i_1,\sigma_2,(\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2))\\
\textsf{h}_0\w(\sigma) & = & (\w_2,i_2i_1,\sigma_2,(\ensuremath{\ell}\xspace_2,\ensuremath{\ell}\xspace_1))
 \end{array}
\]
Here and in what follows it is assumed that
\else

\(
\hspace{-5mm}
 \begin{array}{lcllcllcl}
\textsf{f}_0\w(\sigma) & = & (\w_1,i_1,\sigma_1,\ensuremath{\ell}\xspace_1),~
\textsf{g}_0\w(\sigma) & = & (\w_2,i_2i_1,\sigma_2,(\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2)),
\textrm{ and }
\textsf{h}_0\w(\sigma) & = & (\w_2,i_2i_1,\sigma_2,(\ensuremath{\ell}\xspace_2,\ensuremath{\ell}\xspace_1))
 \end{array}
\)

\noindent
Here and in what follows it is assumed that
\fi
$\textit{new}(\sigma)=(\ensuremath{\ell}\xspace_1,\sigma_1)$ and
$\textit{new}(\sigma_1)=(\ensuremath{\ell}\xspace_2,\sigma_2)$ and
$\w_1=\w\cup\{\ensuremath{\ell}\xspace_1\}$ and $\w_2=\w_1\cup\{\ensuremath{\ell}\xspace_2\}$. Recall that
$\mathfrak{S}\w\subseteq\ensuremath{\mathbb{H}}$. Finally, $i_1:\w\rightarrow\w_1$ and
$i_2:\w_1\rightarrow\w_2$ stand for the obvious inclusions.  We use
analogous definitions for the primed variants.

In order to define $\textsf{f}_{0.5}$ we start with
$u:\w\rightarrow\w'$ and $\sigma\in\mathfrak{S}\w,\sigma'\in\mathfrak{S}\w'$,
$R\in\Rscr(\aEff{})$ such that $(\sigma,u.\sigma')\in R\w$. Define
$u':\w_1\rightarrow\w_1'$ so that $u'i_1=i_1'u$, that is
$u'(\ensuremath{\ell}\xspace\in\w)=u(\ensuremath{\mathsf{L}}\xspace)$, $u'(\ensuremath{\ell}\xspace_1)=\ensuremath{\ell}\xspace_1'$. We now return the
pullback square $\w_1\sq{u'}{1}{1}{u'}\w_1'$ with apex $\w_1'$ and low
point $\w_1$ and the trivial proof that $u'.\ensuremath{\ell}\xspace_1=\ensuremath{\ell}\xspace_1'$. This
settles the definition of $\textsf{f}_{0.5}$, since $R\w_1$ is total since
$R\in\Rscr(\aEff{})$. Notice though, that we cannot avoid the allocation
effect here.

The functions $g_{0.5}$ and $h_{0.5}$ are defined analogously.

We now construct a proof that $\textsf{g}\sim \textsf{h}$, recall that only
$\textsf{g}_0$ and
$\textsf{h}_0$ are needed for this. Given $\w,\sigma$ and the notation from
above this proof amounts to a pullback square
$\w_2\sq{x}{v}{x'}{v'}\w_2'$ such that $xi_2i_1=x'i_2'i_1'u$ and
$x.(\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2)=x'.(\ensuremath{\ell}\xspace_2,\ensuremath{\ell}\xspace_1)$ and $\sigma_2.v \sim
\sigma_2'.v'$. Note that, accidentally, the final abstract stores of
both computations are the same, namely, $\sigma_2$. Now let $f$ be the
bijection that swaps $\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2$ and fixes everything else. We
then put $\sq{x}{v}{x'}{v'} := \sq{1}{f}{f}{1}$.  Now, obviously
$(\ensuremath{\ell}\xspace_1,\ensuremath{\ell}\xspace_2)=f.(\ensuremath{\ell}\xspace_2,\ensuremath{\ell}\xspace_1)$ and $\sim$-equality of
abstract stores is trivial by definition.

\subsection{Heap PERs}
In this section we generalize our earlier collection of effect-dependent program
equivalences
\cite{DBLP:conf/ppdp/BentonKBH07} to the abstract locations of the
Heap PERs instantiation. We first show how the
set factory indeed has the announced effect typings and thus can
participate in effect-dependent equivalences.

\paragraph{Set factory}
Let $\w$ be a world and $\sigma\in\mathfrak{S}\w$. Suppose that $\sigma_1$
arises from $\sigma$ by allocating a fresh set data structure, e.g., a
linked list, with entry point(s) $E$. Let $\ensuremath{\mathsf{L}}\xspace_1$ be the abstract
location describing this fresh data structure, i.e.,
$(\heap,\heap')\in\ensuremath{\mathsf{L}}\xspace_1^R\iff$ the data structures starting from $E$
in $\heap,\heap'$ are well-formed, denote the same set, and do not
overlap with the footprints of all the abstract locations in $\w$. The
footprint $\ensuremath{\mathsf{L}}\xspace_1^F$ comprises the locations that make up this
data structure assuming that $(\heap,\heap)\in\ensuremath{\mathsf{L}}\xspace^R$, otherwise any
value can be chosen. Finally, $\ensuremath{\mathsf{L}}\xspace^G$ contains idempotent
functions, $\iota$, such that $\iota(\heap) = \heap_1$
and $\heap_1$ agree on all concrete locations from
$\dom{\heap}\supseteq\ensuremath{\mathsf{L}}\xspace^F(\heap)$ and, moreover,
$\dom{\heap_1}\supseteq \dom\heap$.

Now for any chosen region $\ensuremath{\mathsf{r}}$ we add $\ensuremath{\mathsf{L}}\xspace_1$ to $\ensuremath{\mathsf{r}}$ to
yield a new world $\w_1$. The function $\textit{setfactory}_0\w\sigma$
then returns $\w_1$ and a tuple of semantic functions for reading,
membership, removal of which we only sketch reading here: If
$u:\w_1\rightarrow \w_2$ and $\sigma_1\in\mathfrak{S}\w_1$ and
$i\in\mathbb{Z}$ then the reading function looks up $i$ in the data
structure starting at the entry points $E$ in $\sigma_1$. (Note that
$\sigma_1\in\mathfrak{S}\w$ asserts that this data structure exists and is
well-formed.) The returned (abstract) store $\sigma_2$ might not be the
same as $\sigma$ because internal reorganizations, e.g., removal of
duplicates, might have occurred. However, no world extension is needed
and
$\sigma_1\sim\sigma_2$ holds. This together with the fact that
the outcome only depends on the $\ensuremath{\mathsf{L}}\xspace^R$ equivalence class \iffull(in the
proof-relevant sense)\fi justifies a read-only typing for reading.

\iffull
In order to model the object-oriented version with a basic type
$\textit{set}_\ensuremath{\mathsf{r}}$ for each region $\ensuremath{\mathsf{r}}$, we can use the p.p.f.\
$\textit{Set}_\ensuremath{\mathsf{r}}\w=\{(\w_0,u,\ensuremath{\mathsf{L}}\xspace) \mid \ensuremath{\mathsf{L}}\xspace\in \w_0(r)$ and
$\ensuremath{\mathsf{L}}\xspace$ is of the above format and $u:\w\rightarrow \w_0$
$\}$. Equality on $\textit{Set}_\ensuremath{\mathsf{r}}\w$ is discrete and one puts
$v.(\w_0,u,\ensuremath{\mathsf{L}}\xspace)=(\w_0,vu,\ensuremath{\mathsf{L}}\xspace)$. The indirection through $\w_0$ is
necessary so that we recognize that a given abstract location is
indeed a ``set''.
\fi
\paragraph{Memoization} For the simple $\textit{memo}$ functional
from Section~\ref{examples} we produce just as in the previous example a
fresh
abstract location $\ensuremath{\mathsf{L}}\xspace$ that contains the two newly allocated
concrete locations, say $\ensuremath{\ell}\xspace_x,\ensuremath{\ell}\xspace_y$, and on which we impose the
invariant $(\heap,\heap')\in \ensuremath{\mathsf{L}}\xspace^R \iff $
$\heap(\ensuremath{\mathsf{L}}\xspace_x),\heap'(\ensuremath{\mathsf{L}}\xspace_x)$ contain the same integer value, say $i$
and that $\heap(\ensuremath{\mathsf{L}}\xspace_y),\heap'(\ensuremath{\mathsf{L}}\xspace_y)$ both contain the integer value
$f(i)$ where $f$ is the pure function to be memoised.\iffull We see in
Lemma~\ref{lemmasix} that if a function is semantically pure (empty
effect) then there is a world- and store-independent function
describing its action.\fi

\iffull
\subsubsection{Effect-dependent equivalences}
\else
\paragraph{Effect-dependent equivalences} Consider the following
notation
\fi

\iffull
Before we prove the soundness of a number of program equivalences,
we introduce some notation. Given a set of effects $\varepsilon$, we write
$\rdsin{\varepsilon} = \{\ensuremath{\mathsf{r}} \mid \rEff\ensuremath{\mathsf{r}} \in \varepsilon\}$, $\wrsin{\varepsilon} =
\{\ensuremath{\mathsf{r}} \mid \wEff\ensuremath{\mathsf{r}} \in \varepsilon\}$,  $\alsin{\varepsilon} = \{\ensuremath{\mathsf{r}} \mid
\aEff\ensuremath{\mathsf{r}} \in \varepsilon\}$ and $\regs{\varepsilon} = \rdsin{\varepsilon} \cup \wrsin{\varepsilon}
\cup \alsin{\varepsilon}$. Moreover, the set ${\ensuremath{\mathit{nwrs}}}(\varepsilon) = \regs{\varepsilon} \setminus
\wrsin{\varepsilon}$. We also introduce the following piece of notation for
$\sigma, \sigma' \in \mathfrak{S} \w$:
\[
\begin{array}{c}
\sigma \sim_{\rdsin{\varepsilon, \w}} \sigma' \iff \forall \ensuremath{\mathsf{L}}\xspace \in
\w(\rdsin{\varepsilon}). (\sigma, \sigma') \in \ensuremath{\mathsf{L}}\xspace^R \\
\sigma \sim_{{\ensuremath{\mathit{nwrs}}}(\varepsilon, \w)} \sigma' \iff \forall \ensuremath{\mathsf{L}}\xspace \in
\w({\ensuremath{\mathit{nwrs}}}(\varepsilon)). (\sigma, \sigma') \in \ensuremath{\mathsf{L}}\xspace^R
\end{array}
\]
which specify that the abstract heaps $\sigma$ and $\sigma'$ are
\else

\(
\begin{array}{c}
\sigma \sim_{\rdsin{\varepsilon, \w}} \sigma' \iff \forall \ensuremath{\mathsf{L}}\xspace \in
\w(\rdsin{\varepsilon}). (\sigma, \sigma') \in \ensuremath{\mathsf{L}}\xspace^R \\
\sigma \sim_{{\ensuremath{\mathit{nwrs}}}(\varepsilon, \w)} \sigma' \iff \forall \ensuremath{\mathsf{L}}\xspace \in
\w({\ensuremath{\mathit{nwrs}}}(\varepsilon)). (\sigma, \sigma') \in \ensuremath{\mathsf{L}}\xspace^R
\end{array}
\)

\noindent
which specify that the abstract heaps $\sigma$ and $\sigma'$ are
\fi
equivalent on all the abstract locations $\ensuremath{\mathsf{L}}\xspace$ in regions associated,
respectively, to read effects and no-writes in $\varepsilon$.

\begin{lemma}\label{lemmasix}
\label{lem:invariant}
Let $\Gamma \vdash e : \ety{\tau}{\varepsilon}$. For any world $\w \in \ensuremath{\mathbf{W}}\xspace$,
and context $\gamma \in \sem{\Gamma}\w$, whenever $\sigma_0 , \sigma_0' \in
\mathfrak{S}\w$ such that $\sigma_0
\sim_{\rdsin{\varepsilon, \w}} \sigma_0'$, then $\cval(\sigma_0)$ and
$\cval(\sigma_0')$ where $\cval =\sem{\Gamma \vdash e :
\ety{\tau}{\varepsilon}}\w(\gamma)$ are
equally defined  and if $\cval(\sigma_0)=(\w_1, u, \sigma_1,
\val)$ and
$\cval(\sigma_0') = (\w_1', u', \sigma_1', \val')$
then there exist (continuously!) a pullback
 $\w_1 \sq{x}{v}{x'}{v'} \w_1'$ with apex
$\overline{\w}$ and low point $\und{\w}$ and a proof of $x.\val\sim x'.\val'$ such that $xu=x'u'$ and the following is satisfied:
\begin{compactenum}
 \item for all $\ensuremath{\mathsf{L}}\xspace \in \w$, we have either: $(\sigma_0,
\sigma_1.u) \in \ensuremath{\mathsf{L}}\xspace^R$
and $(\sigma_0', \sigma_1'.u') \in \ensuremath{\mathsf{L}}\xspace^R$ (remain
equivalent) or
$(\sigma_1.u, \sigma_1'.u') \in \ensuremath{\mathsf{L}}\xspace^R$ (equally modified);
 \item if $\ensuremath{\mathsf{L}}\xspace \in \w({\ensuremath{\mathit{nwrs}}}(\varepsilon))$, then $(\sigma_0,
\sigma_1.u) \in \ensuremath{\mathsf{L}}\xspace^R$ and $(\sigma_0',
\sigma_1'.u') \in \ensuremath{\mathsf{L}}\xspace^R$.

\item There exists a morphism $\cval' \in \sem{\Gamma}\to T_\varepsilon
\sem{\tau}$, such that  $\cval' \sim \cval$ and if
$\cval'(\w)(\gamma)\sigma_0 = (\w_\star, u_\star, \sigma_\star,
\val_\star)$, then for all regions $\ensuremath{\mathsf{r}} \notin \alsin{\varepsilon}$,
$\w_\star(\ensuremath{\mathsf{r}}) = \w(\ensuremath{\mathsf{r}})$.
\end{compactenum}
\end{lemma}
\iffull\begin{proof}
The proof that the values are equal in $\und{\w}$ follows directly from
the definition of computations and effects.

For the first part,  we use the following relation $R$ defined for all
worlds $\w_1$, such that $u : \w \to \w_1$:

\(
\begin{array}{l}
 \{(\sigma, \sigma') \mid \sigma \sim_{\rdsin{\varepsilon, \w}} \sigma'
\land \forall \ensuremath{\mathsf{L}}\xspace \in \w.\\
 \qquad (\sigma.u, \sigma_0) \in \ensuremath{\mathsf{L}}\xspace^R \land
(\sigma'.u, \sigma_0') \in \ensuremath{\mathsf{L}}\xspace^R \lor (\sigma.u, \sigma'.u) \in
\ensuremath{\mathsf{L}}\xspace^R\}
\end{array}
\)

\noindent
Otherwise, for the worlds $\w_2$ not reachable from \w, the relation
$R\w_2$ is the trivial set. Notice that $R \in \Rscr(\varepsilon)$ and it is
contravariant. The claim then
follows directly.

The proof of the second part follows in a similar fashion, but we use the
following relation:

\(
\{(\sigma, \sigma') \mid \sigma \sim_{\rdsin{\varepsilon, \w}} \sigma'
\land \sigma \sim_{{\ensuremath{\mathit{nwrs}}}(\varepsilon, \w)} \sigma_0.u \}
\)

\noindent
And we use a similar relation for showing that $\sigma_0'$ and
$\sigma_1'.u'$ agree on the not written locations ${\ensuremath{\mathit{nwrs}}}(\varepsilon, \w)$.

For the third property, first, we show that there is an
isomorphism between $\w(\ensuremath{\mathsf{r}})$ and $\und{\w}(\ensuremath{\mathsf{r}})$ for all regions
$\ensuremath{\mathsf{r}} \notin \alsin{\ensuremath{\mathsf{r}}}$ by using the following relation:

\(
\{(\sigma, \sigma') \mid \sigma \sim \sigma' \land \forall
\ensuremath{\mathsf{r}} \notin \alsin{\varepsilon}. \#_\ensuremath{\mathsf{r}}(\sigma), \#_\ensuremath{\mathsf{r}}(\sigma')
\leq \#_\ensuremath{\mathsf{r}}(\w) \}
\)

\noindent
where $\#_\ensuremath{\mathsf{r}}$ denotes the number of abstract locations coloured with
$\ensuremath{\mathsf{r}}$.
Clearly, $R \in
\Rscr(\varepsilon)$ as $\varepsilon$ does not contain any allocation effects. This gives
us one direction, while the other direction is obtained by the universal
property of pullbacks. Given this property, one can easily construct the
function $\cval'$.
\end{proof}
\begin{proposition}\label{compr}
(commuting computations) Suppose that:
$
 \Gamma \vdash e_1 : \ety{\tau_1}{\varepsilon_1}$ and
$\Gamma \vdash e_2 :
\ety{\tau_2}{\varepsilon_2}
$,
where  $\rdsin{\varepsilon_1} \cap \wrsin{\varepsilon_2} = \rdsin{\varepsilon_2} \cap
\wrsin{\varepsilon_1}=
\wrsin{\varepsilon_1} \cap \wrsin{\varepsilon_2} = \emptyset$. Let
\[
 \begin{array}{l}
  e = \letin{x}{e_1} \letin{y}{e_2} (x, y) \quad \textrm{and} \quad
  e' = \letin{y}{e_2} \letin{x}{e_1} (x, y)
 \end{array}
\]
then $\sem{\Gamma \vdash e : \ety{ \tau_1 \times \tau_2 }{\varepsilon_1\cup
\varepsilon_2}} \sim \sem{\Gamma \vdash e' : \ety{ \tau_1 \times \tau_2
}{\varepsilon_1\cup \varepsilon_2}}$.
\end{proposition}

\begin{proof}
Assume a world \w and a context $\gamma \in \sem{\Gamma}\w$.
Let $\cval_i = \sem{\Gamma \vdash e_i : \ety{\tau_i}{\varepsilon_i}}$ for
$i = 1,2$.

It is enough to assume a pullback
$\w \sq{1}{1}{1}{1} \w$, and an abstract heap $\sigma_0 \in
\mathfrak{S} \w$.
Assume that these functions are defined as follows:

\(
 \begin{array}{l}
 \cval_1(\w)(\gamma)\sigma_0 = (\w \uplus \w_1, u_1, \sigma_1, \val_1)\\
 \cval_2(\w\uplus\w_1)(u_1.\gamma) \sigma_1 = (\w \uplus \w_1 \uplus
\w_2, u_2, \sigma_2, \val_2)\\
 \cval_2'(\w)(\gamma)\sigma_0 = (\w \uplus \w_1', u_1', \sigma_1',
\val_1')\\
 \cval_1'(\w\uplus\w_2')(u_1'.\gamma) \sigma_1' = (\w \uplus \w_1'
\uplus \w_2', u_2', \sigma_2',\val_2')
 \end{array}
\)

\noindent
One can easily show that when one of these functions is undefined, then
the corresponding function is also undefined.

We need to show that there is a proof $\w \uplus \w_1 \uplus \w_2
\sq{x}{v}{x'}{v'} \w \uplus \w_1' \uplus \w_2'$ such that
$p : \sigma_2.v \sim \sigma_2'.v'$ and $p_1 : xu_2.\val_1 \sim x'.\val_2'$
and $p_2 : x.\val_2 \sim x'u_2'.\val_1'$.
Decompose $\w = \w_0 \uplus \q_1 \uplus \q_2$, where
$\w(\wrsin{\varepsilon_i}) \subseteq \q_i$.
The existence of such decomposition follows from the disjointness of write
effects in $\varepsilon_1$ and $\varepsilon_2$.

From Lemma~\ref{lem:invariant} and from
the disjointness of reads and writes, it is the case that $\sigma_0$ and
$\sigma_1'$ agree on the locations in $\w_0 \uplus \q_1$.
That is, there is a proof $p : \sigma_0.1 \sim \sigma_1'.x_1$, defined
using the proof $\w_0 \uplus \q_1 \sq{x_1}{1}{1}{x_1} \w_0
\uplus \q_1 \uplus \w_2'
$, where $x_1 : \w_0 \uplus \q_1 \to \w_0 \uplus \q_1 \uplus \w_2'$.
Applying $(e_1)_1$ to the objects above,
we get the pullback $\w_0 \uplus \q_1 \uplus \w_1 \sq{x_2}{v_2}{x_2'}{v_2'}
\w_0 \uplus \q_1
\uplus
\w_2' \uplus \w_1'$, and  proof $q : x_2.\val_1 \sim
x_2'.\val_2'$. Symmetrically, we obtain the proofs
$\w_0 \uplus \q_2 \uplus \w_2 \sq{x_3}{v_3}{x_3'}{v_3'} \w_0 \uplus \q_2
\uplus \w_1' \uplus \w_2'$, and  $q' : x_3.\val_2 \sim
x_3'.\val_1'$. Hence, there is also a proof in the larger world $cod(x)$.

To see informally that the final heaps $\sigma_2$ and $\sigma_2'$ are
equal, we use
the following facts obtained using Lemma~\ref{lem:invariant}: $\sigma_2$
and $\sigma_1$ agree on the locations in $\w_0 \uplus \q_1$; moreover,
$\sigma_2'$ and $\sigma_1$ agree on the locations in $\w_0 \uplus \q_1$;
hence $\sigma_2$ and $\sigma_2'$ agree on the locations in $\w_0 \uplus
\q_1$. Symmetrically, we can also argue that $\sigma_2$ and $\sigma_2'$
agree on the locations in $\w_0 \uplus \q_2$. Composing these proofs
(see comment after Lemma~\ref{lem:unique-upto-sim} why this is allowed),
we get that $\sigma_2$ and $\sigma_2'$ agree on the locations in $\w$.
Finally, since the locations allocated by one computation are not used by
the other computation, the final heaps are equal at the
apex world.
\end{proof}

The following propositions are also provable. All propositions are proved
in a similar way as the soundness proof of the commuting case, using
Lemma~\ref{lem:invariant} when needed. For instance, the soundness proof
of the duplicated computation uses the third case in
Lemma~\ref{lem:invariant}.

\begin{proposition}[dead computation]\label{dead}
Suppose that
$\Gamma \vdash e : \ety{\keywd{unit}}{\varepsilon}$,
that \iffull $\wrsin{\varepsilon}=\emptyset$ \else
$\varepsilon$ contains no writes \fi and that $\sem{\Gamma\vdash
e: \ety{\keywd{unit}}{\varepsilon}}\w(\gamma)(\sigma)$ is defined for all
$\w,\gamma\in\sem{\Gamma}\w, \sigma\in\mathfrak{S}\w$.
Then if for all worlds \w, all contexts $\gamma \in
\sem{\Gamma}\w$, and abstract heaps $\sigma \in \mathfrak{S}\w$,
the function $\sem{\Gamma \vdash e}(\w)(\gamma)(\sigma)$ is defined,
then $\sem{\Gamma \vdash e : \ety{\keywd{unit}}{\varepsilon}} \sim \sem{\Gamma
\vdash \keywd{()} : \ety{\keywd{unit}}{\varepsilon}}$.
\end{proposition}

\begin{proof}
Assume a world \w and a context $\gamma \in \sem{\Gamma}\w$.
Let $\cval = \sem{\Gamma \vdash e : \ety{\tau}{\varepsilon}}$.
It is enough to assume a pullback
$\w \sq{1}{1}{1}{1} \w$, and an abstract heap $\sigma_0 \in
\mathfrak{S} \w$. Let $\cval(\w)(\gamma)\sigma_0  =  (\w, 1, \sigma_1,
\val_1)$. We need to construct a pullback such that $\val_1$ is equivalent
to $\keywd{()}$ in its apex and $\sigma_1$ is equivalent to $\sigma_0$ in
its low point. Consider the pullback $\w_1 \sq{1}{u}{u}{1} \w$. Clearly
$\val_1 = \keywd{()}$, and therefore the values are equivalent in $\w_1$.
Moreover, from the fact that $\wrsin{\varepsilon} =
\emptyset$, $\sigma_1$ and $\sigma_0$ agree on all locations in $\w$.
Hence, $\sigma_1.u \sim \sigma_0$, which finishes the proof.
\end{proof}

\begin{proposition}[duplicated computation]\label{dupl}
  Suppose that $\Gamma \vdash e:\ety{\tau}{\varepsilon}$ and suppose
that
  $\mathrm{rds}(\varepsilon)\cap\mathrm{wrs}(\varepsilon)=\mathrm{als}(\varepsilon)=\emptyset$. Thus, $e$
  reads and writes on disjoint portions of the store and makes no
  allocations. The the terms  $e_1$ and $e_2$ below
\[\begin{array}{l}
\letin{x}{e}{(x,x)} ~\textrm{ and }~ \letin{x}{e} \letin{y}{e}{(x,y)}
\end{array}
\]
 are contextually equivalent. That is
formally $\sem{\Gamma \vdash e_1 : \ety{\tau \times \tau}{\varepsilon}} \sim
\sem{\Gamma \vdash e_2 : \ety{\tau \times \tau}{\varepsilon}}$.
\end{proposition}

\begin{proof}
Assume a world \w and a context $\gamma \in \sem{\Gamma}\w$.
Let $\cval = \sem{\Gamma \vdash e : \ety{\tau}{\varepsilon}}$.
It is enough to assume a pullback
$\w \sq{1}{1}{1}{1} \w$, and an abstract heap $\sigma_0 \in
\mathfrak{S} \w$.
From Lemma~\ref{lemmasix} and since these functions do not allocate, we
can assume that they do not cause any world extension and are therefore
defined as follows:
\[
 \begin{array}{lcl}
 \cval(\w)(\gamma)\sigma_0  =  (\w, 1, \sigma_1, \val_1) &
\textrm{and}&
  \cval(\w)(\gamma)\sigma_1  =  (\w, 1, \sigma_2, \val_2).
 \end{array}
\]
We need to show that the values $\val_1$ and $\val_2$ are equivalent and
the heaps $\sigma_1$, obtained by applying once $e$, and $\sigma_2$,
obtained by applying twice $e$, are also equal.

Decompose $\w = \w_0 \uplus \w_r \uplus \w_w $, where $\w_r$ contains all
the regions read by $e$ and $\w_w$ all the regions written by $e$. This is
possible because of the disjointness of of $e$'s read and write effects.
From Lemma~\ref{lemmasix} and the disjointness of  $e$'s read and write
effects, we have that $\sigma_0$ and $\sigma_1$ agree on the regions read
by $e$, that is, $\sigma_0 \sim_{\rdsin{\varepsilon, \w}} \sigma_1$. Hence, again
from Lemma~\ref{lemmasix}, we have that the values $\val_1$ and $\val_2$
are equal. Moreover, the locations in $\w_w$ are equaly written, while the
locations in $\w_0 \uplus \w_r$ are left unchanged, that is,
$\sigma_1$ and $\sigma_2$ agree on the location in $\w$.
\end{proof}

\begin{proposition}[pure lambda hoist]\label{hoist}
Suppose that $
\Gamma\vdash e: \ety{Z}{\emptyset}$ and
$\Gamma,x{:}X,y{:}Z\vdash e': \ety{Y}{\varepsilon}$
Let $e_1$ and $e_2$ be respectively $
\lambda x.\letin{y}{e} {e'}$ and
$\letin{y}{e}{\lambda x.e'}$.
Then $\sem{\Gamma\vdash  e_1 :
\ety{(\valty{X\effto\varepsilon
Y})}{\emptyset}} \sim
\sem{\Gamma\vdash  e_2 : \ety{(\valty{X\effto\varepsilon
Y})}{\emptyset}}$.
\end{proposition}

\begin{proof}
Assume a world \w and a context $\gamma \in \sem{\Gamma}\w$.
Let $\cval = \sem{\Gamma \vdash e : \ety{\tau}{\varepsilon}}$ and
$\cval' = \sem{\Gamma, x: X, y: Z \vdash e' : \ety{\tau}{\varepsilon}}$.
It is enough to assume a pullback
$\w \sq{1}{1}{1}{1} \w$, and an abstract heap $\sigma_0 \in
\mathfrak{S} \w$. Since $e$ has no effects, we have no world extension:
\[
 \cval(\w)(\gamma)\sigma_0  =  (\w, 1, \sigma_1', \val_1')
\]
Moreover, from Lemma~\ref{lemmasix}, $\sigma_1$ and $\sigma_0$ agree on
all locations. We now show that
\[
\sem{\Gamma\vdash  \lambda x.\letin{y}{e} {e'(x,y)} : (\valty{X\effto\varepsilon
Y})}
\sim
\sem{\Gamma\vdash \lambda x.e'(x,\val_1') : (\valty{X\effto\varepsilon
Y})}
\]
In order to prove this, assume a morphism $v : \w \to \w_1$ and $a \in
\sem{X}\w_1$. We need then to prove that the computations resulting from
applying $a$ to the functions above are equivalent in the pullback
$\w_1\sq{1}{1}{1}{1}\w_1$. For this, assume an abstract heap $\sigma \in
\mathfrak{S} \w_1$. Since $e$ has no effect, we have no world extension:
\[
\begin{array}{l}
 \cval(\w_1)(\gamma)\sigma  =  (\w_1, 1, \sigma_1, \val_1) \\
 \cval'(\w_1)(\gamma, a, \val_1 )\sigma_1  =  (\w_2, 1, \sigma_2, \val_2)\\
\cval'(\w_1)(\gamma, a, \val_1' )\sigma  =  (\w_2', 1, \sigma_1', \val_2)
\end{array}
\]
Since $e$ is pure, we have $\val_1 = v.\val_1'$ and from
Lemma~\ref{lemmasix} we have that $\sigma_1$ and $\sigma$ agree on all
locations in $\w_1$ and in particular on locations read by $e'$. Hence,
again by Lemma~\ref{lemmasix} the pullback proof exists where $\sigma_2$
and
$\sigma_1'$ are equal in its low point and the resulting values are equal
in its apex.
\end{proof}
\else
We can validate all the effect-dependent program equivalences ``dead,
commuting, duplicated computation'' and ``pure lambda hoist'', as well
as the ``masking rule'' from previous work \cite{DBLP:conf/aplas/BentonKHB06} in our new, more powerful,
setting.
To give an impression of the
formulation of these validations we state the corresponding proposition for
``dead computation'' which is particularly interesting in that it contains
a termination precondition. The proof, and details of the other
equations are in the
\ifapp
appendix,
\else
long version,
\fi
which also
contains a validation of loop unrolling optimisation
described by Tristan and Leroy \cite{tristan10popl}.
 \begin{proposition}[dead computation]\label{dead}
Suppose that
$\Gamma \vdash e : \ety{\keywd{unit}}{\varepsilon}$,
that $\wrsin{\varepsilon}=\emptyset$ and that $\sem{\Gamma\vdash
e: \ety{\keywd{unit}}{\varepsilon}}\w(\gamma)(\sigma)$ is defined for all
$\w,\gamma\in\sem{\Gamma}\w, \sigma\in\mathfrak{S}\w$.
Then if for all worlds \w, all contexts $\gamma \in
\sem{\Gamma}\w$, and abstract heaps $\sigma \in \mathfrak{S}\w$,
the function $\sem{\Gamma \vdash e}(\w)(\gamma)(\sigma)$ is defined,
then $\sem{\Gamma \vdash e : \ety{\keywd{unit}}{\varepsilon}} \sim \sem{\Gamma
\vdash \keywd{()} : \ety{\keywd{unit}}{\varepsilon}}$.
\end{proposition}
 \fi
\iffull
\begin{figure*}[t]
\begin{center}
\begin{small}
\begin{tabular}{l@{\quad}l@{\quad}l@{\quad}l}
Body of Loop & Prolog & Steady Program & Epilogue\\
\texttt{x := load(p);} & \texttt{p1 := p;} &
\texttt{store(p1, y);}
\textbf{[$\wEff{\ensuremath{\mathsf{r}}_1}$]} & \texttt{store(p1, y);}
\textbf{[$\wEff{\ensuremath{\mathsf{r}}_1}$]}\\

\texttt{y := x * c;} & \texttt{p2 := p;} & \texttt{p1 := p2 + 8;} &
\texttt{y := x2 * c;} \\

\texttt{store(p, y);} & \texttt{x1 := x;} & \texttt{y := x2 * c;}
& \texttt{store(p2, y);} \textbf{[$\wEff{\ensuremath{\mathsf{r}}_2}$]}\\

\texttt{p := p + 8;} & \texttt{x2 := x;} & \texttt{x1 := load(p1);
\textbf{[$\rEff{\ensuremath{\mathsf{r}}_1}$]}} & \texttt{x := x2;}\\

\texttt{i := i + 1;} & \texttt{x1 := load(p1);}
\textbf{[$\rEff{\ensuremath{\mathsf{r}}_1}$]} &
\texttt{store(p2, y);} \textbf{[$\wEff{\ensuremath{\mathsf{r}}_2}$]}
& \texttt{p := p2;}\\

& \texttt{p2 := p1 + 8;} & \texttt{p2 = p1 + 8;}\\
& \texttt{x2 := load(p2);} \textbf{[$\rEff{\ensuremath{\mathsf{r}}_2}$]} &
\texttt{y
= x1 * c;}\\

& \texttt{y := x1 * c;} & \texttt{y = load(p2);
\textbf{[$\rEff{\ensuremath{\mathsf{r}}_2}$]}}\\

& \texttt{i := i + 2;} & \texttt{i := i + 2;}\\
\end{tabular}
\end{small}
\vspace{-2mm}
\end{center}
\caption{Program obtained from the loop unrolling technique. Here
\texttt{p}, \texttt{p1} and \texttt{p2} are pointers and all \texttt{load}
and \texttt{store} operations are on 64 bit numbers (float).}
\label{fig:loop-unrolling}
\vspace{-4mm}
\end{figure*}

\subsection{Loop Unrolling}
Loop unrolling is a software pipelining technique used to enhance the use
of parallel processing. The idea is instead of iterating a loop
in a sequential manner, one attempts to process a number of iterations
of the loop at the same time using multiple processors.

As described in \cite{tristan10popl} implementing and proving the
correctness of loop unrolling techniques is hard as
one needs to demonstrate that the program resulting from loop unrolling
that can be executed in parallel is equivalent to the original sequential
program. We briefly illustrate the power of our system with regions and
effects by one of the running examples in \cite{tristan10popl}. Consider
a loop program whose body is depicted in Figure~\ref{fig:loop-unrolling}.
Intuitively, this program is multiplying all the elements of an array of
float values by the value \texttt{c}. Clearly, instead of executing this
program sequentially, we can execute different iterations in parallel.
In particular, after applying the loop unrolling optimization to a program,
one obtains a program that is divided in three parts: the prolog, that
initializes all the variables, the steady state, that is iterated, and the
epilogue, that is executed when the loop condition is no longer true and
the loop is over. Figure~\ref{fig:loop-unrolling} contains the program
obtained by loop unrolling two iterations of the program above. The Prolog
and the Epilogue are executed at the beginning and the end, respectively,
while the Steady Program may be executed several times.

The task is to show that the optimized program is equivalent to the
sequential program above. Using the unrolling equations from
Lemmas~\ref{fixlse} we can unroll the loop twice
($n=2$) and extract a prologue. We can then conclude with
effect-dependent equivalences, in particular Prop.~\ref{compr} as
follows. We use two regions $\ensuremath{\mathsf{r}}_1$
and $\ensuremath{\mathsf{r}}_2$. All even elements of the array, that is, \texttt{p},
\texttt{p + 16}, \texttt{p + 32}, \ldots, belong to the region $\ensuremath{\mathsf{r}}_1$,
while all odd elements, that is, \texttt{p + 8},
\texttt{p + 24}, \texttt{p + 40}, \ldots, belong to the region $\ensuremath{\mathsf{r}}_2$.
Given this setting, the read and write effects are as shown in
Figure~\ref{fig:loop-unrolling}. It is now a simple exercise to show that
any execution of the optimized program is equivalent to an execution of
the sequential program. For instance, any instruction with a read effect
on $\ensuremath{\mathsf{r}}_1$ can be permuted so that it appears immediately before the
following instruction with write effect $\ensuremath{\mathsf{r}}_1$ on the same region
$\ensuremath{\mathsf{r}}_1$. This is possible because the only effect between these two
instructions is a read on the other region $\ensuremath{\mathsf{r}}_2$. The same is true
for permuting instructions that read on $\ensuremath{\mathsf{r}}_2$.

\fi
\subsection{State Dependent Abstract Data Types (ADT)}
We prove the equivalence of a number of programs involving state dependent
abstract data types.

\paragraph{Awkward Example}
 The first example is Pitts and Stark's classic \emph{awkward}
example\cite{pitts98high}. Consider the
following two programs:
\iffull
\[
 e_1 = \letin{x}{\myref{0}} \lambda f. x:= 1; f(); !x
\qquad\textrm{and}\qquad
 e_2 = \lambda f. f(); 1.
\]
Intuitively, the expressions $e_1$ and $e_2$ are equivalent as they both
\else

\(
 e_1 = \letin{x}{\myref{0}} \lambda f. x:= 1; f(); !x
\qquad\textrm{and}\qquad
 e_2 = \lambda f. f(); 1.
\)

\noindent
Intuitively, the expressions $e_1$ and $e_2$ are equivalent as they both
\fi
return the value $1$, although $e_1$ uses a fresh location to do so.
We can formally prove the equivalence of these functions as follows:
Assign the region where $x$ is allocated as $\ensuremath{\mathsf{r}}$. If $f$ has the type
$\keywd{unit} \effto{\varepsilon} \keywd{unit}$ with effects $\varepsilon$, then $e_1$ has
type $\ety{(\keywd{unit} \effto{\varepsilon} \keywd{unit}) \effto{\varepsilon, \rEff{\ensuremath{\mathsf{r}}},
\wEff{\ensuremath{\mathsf{r}}}}
\keywd{int}}{\varepsilon, \aEff{\ensuremath{\mathsf{r}}}}$, while
$e_2$ has type $\ety{(\keywd{unit} \effto{\varepsilon} \keywd{unit}) \effto{\varepsilon}
\keywd{int}}{\varepsilon}$. Notice that  $\varepsilon$ may contain
$\rEff{\ensuremath{\mathsf{r}}}$
or $\wEff{\ensuremath{\mathsf{r}}}$ or both. Moreover,
assume that the footprint of a location in
region \ensuremath{\mathsf{r}}\ consists of a single concrete location \ensuremath{\ell}\xspace, and that the
guarantee of a location $\ensuremath{\ell}\xspace^G$ consist of a single function
$\mathit{write}_1$ such that $\mathit{write}_1(\heap) = \heap'$ where
$\heap'(\ensuremath{\ell}\xspace) = 1$ and $\heap'(\ensuremath{\ell}\xspace') = \heap(\ensuremath{\ell}\xspace')$ for all other
locations. Clearly $e_1$ has such a write effect.

For proving the equivalence of $e_1$ and $e_2$, assume a world $\w$ and an
abstract heap $\sigma$. Let $\sem{e_1}\w\sigma = (\w \uplus \w_1 \uplus
\w_r, u_1, \val_1, \sigma_1)$ and $\sem{e_2}\w\sigma = (\w \uplus \w_1,
u_1, \val_2, \sigma_2)$. We need to construct a pullback square $\w \uplus
\w_1 \uplus \w_r\sq{}{}{}{}\w \uplus \w_1$ such that the values $\val_1$
and $\val_2$ are equal in its apex and $\sigma_1$ and $\sigma_2$ are equal
in its low point. Since $\wEff \ensuremath{\mathsf{r}}$ is in the effects of $e_1$, we
have that $\val_1 = 1$. We also have $\val_2 = 1$ trivially. Hence
$\val_1$ and $\val_2$ are equal in the apex of the pullback square $\w
\uplus
\w_1 \uplus \w_r\sq{}{}{}{}\w \uplus \w_1$. Similarly, $\sigma_1$ when
taken to the low point of the square, that is, where the locations in
$\w_r$ are forgotten, the resulting heap is equivalent to $\sigma_2$.

\paragraph{Modified Awkward Example}
Consider now the following variant of the Awkward example, due to
Dreyer et al.\cite{dreyer10icfp}:
\iffull
\[
 e_1 = \letin{x}{\myref{0}} \lambda f. x:= 0; f(); x:= 1; f(); !x
~\textrm{ and }~
 e_2 = \lambda f. f();f(); 1.
\]
The difference is that in the first program $x$ is written to $0$ and the
\else

\(
 e_1 = \letin{x}{\myref{0}} \lambda f. x:= 0; f(); x:= 1; f(); !x
~\textrm{ and }~
 e_2 = \lambda f. f();f(); 1.
\)

\noindent
The difference is that in the first program $x$ is written to $0$ and the
\fi
call-back function is used twice. Interestingly, however, the solution
given for the Awkward example works just fine. We can prove semantically
that the type of the program $e_1$ has the same type as before in the
Awkward example, where the only writes allowed on abstract location
assigned for $x$ is to write one.
Therefore, if $f$ has effect of writing on the region $\ensuremath{\mathsf{r}}$, it will set
$x$ to one.

\paragraph{Callback with Lock Example}
We now show equivalence of the following programs, also due to Dreyer
et al.\cite{dreyer10icfp}:
\iffull
\[
\begin{array}{l@{\quad}l}
 e_1 = \letin{b}{\myref{\keywd{true}}} \letin{x}{\myref{0}}
& e_2 = \letin{b}{\myref{\keywd{true}}} \letin{x}{\myref{0}}\\
\quad \langle \lambda f. \keywd{if}~{!b}~\keywd{then}
& \quad \langle \lambda f. \keywd{if}~{!b}~\keywd{then}\\
\quad\quad({b:= \keywd{false}};
f(); x := !x + 1; b:= \keywd{true})
&
\quad\quad({b:= \keywd{false}};
\letin{n}{!x} f();
\\
\quad ~\keywd{else}~(), \lambda\_.!x\rangle
& \quad\quad x := n + 1; b:= \keywd{true})
\\& \quad ~\keywd{else}~(), \lambda\_.!x\rangle
\end{array}
\]
\else

\(
\hspace{-9mm}
\begin{array}{l@{\quad}l}
 e_1 = \letin{b}{\myref{\keywd{true}}} \letin{x}{\myref{0}}
& e_2 = \letin{b}{\myref{\keywd{true}}} \letin{x}{\myref{0}}\\
\quad \langle \lambda f. \keywd{if}~{!b}~\keywd{then}
& \quad \langle \lambda f. \keywd{if}~{!b}~\keywd{then}\\
\quad\quad({b:= \keywd{false}};
f(); x := !x + 1; b:= \keywd{true})
&
\quad\quad({b:= \keywd{false}};
\letin{n}{!x} f();
\\
\quad ~\keywd{else}~(), \lambda\_.!x\rangle
& \quad\quad x := n + 1; b:= \keywd{true})
\\& \quad ~\keywd{else}~(), \lambda\_.!x\rangle
\end{array}
\)

\noindent
\fi
Both programs produce a pair of functions, one incrementing the
value stored in $x$ and the second returning the value stored in $x$.
The boolean reference $b$ serves as lock in the
incrementing function.
Once this function is called the value in $b$ is set to
$\keywd{false}$ and only after calling the call-back, the value in
$x$ is incremented is $b$ set again to $\keywd{true}$. However, the
implementation of
the increment function is different. While the program to the
left calls the call-back function $f()$ and then increments the value of
$x$ using the value stored in $x$, the program to the right remembers (in
$n$) the value of $x$ before the call-back is called and then uses it to
increment the value stored in $x$.

Assume that $x$ and $b$ are in the footprint of the same abstract location
($\ensuremath{\mathsf{L}}\xspace$) in the
region $\ensuremath{\mathsf{r}}$. We show that these programs are equivalent under the type
\iffull
\[
\ety{(\keywd{unit} \effto{\varepsilon} \keywd{unit}) \effto{\varepsilon, \wEff{\ensuremath{\mathsf{r}}},
\rEff{\ensuremath{\mathsf{r}}}} \keywd{unit}) \times (\keywd{unit} \effto{\rEff{\ensuremath{\mathsf{r}}}}
\keywd{unit})}{\aEff{\ensuremath{\mathsf{r}}}, \varepsilon},
\]
 where $\varepsilon$ may contain the effects
\else

\(
\ety{(\keywd{unit} \effto{\varepsilon} \keywd{unit}) \effto{\varepsilon, \wEff{\ensuremath{\mathsf{r}}},
\rEff{\ensuremath{\mathsf{r}}}} \keywd{unit}) \times (\keywd{unit} \effto{\rEff{\ensuremath{\mathsf{r}}}}
\keywd{unit})}{\aEff{\ensuremath{\mathsf{r}}}, \varepsilon},
\)

\noindent
 where $\varepsilon$ may contain the effects
\fi
$\wEff{\ensuremath{\mathsf{r}}}, \rEff{\ensuremath{\mathsf{r}}}$. In particular, the location $\ensuremath{\mathsf{L}}\xspace$ is
specified as follows: its footprint consists only of the concrete
locations storing $x$ and $b$, written $\ensuremath{\ell}\xspace_b$ and $\ensuremath{\ell}\xspace_x$, while its
rely-condition is equality. The more interesting is its guarantee condition
($\ensuremath{\mathsf{L}}\xspace^G$), which contains
the following idempotent functions $f_i$ for $i \in \mathbb{N}$:
$f_i(\heap) = \heap$ if $\heap(\ensuremath{\ell}\xspace_b) = \keywd{false}$ and $f_i(\heap) =
\heap'$ if $\heap(\ensuremath{\ell}\xspace_b) = \keywd{true}$, where $\heap'(\ensuremath{\ell}\xspace_x) = i$ if
$\heap(\ensuremath{\ell}\xspace_x) \leq i$ and $\heap'(\ensuremath{\ell}\xspace_x) = \heap(\ensuremath{\ell}\xspace_x)$;
moreover, the value of $b$ is unchanged, that is, $\heap'(\ensuremath{\ell}\xspace_b) =
\heap(\ensuremath{\ell}\xspace_b)$.
It is easy to check that these functions are idempotent as well as their
composition.

First, notice that indeed the two functions above have type $\wEff{\ensuremath{\mathsf{r}}}$
as the increment of $x$ is captured by using some write function
$f_i$
and moreover $b$ is $\keywd{true}$. Now, to show that the two programs above
are equivalent, we need to show that the value stored in $x$ before and
after the call back is called is the same. This is the case, as even if
$\wEff{\ensuremath{\mathsf{r}}} \in \varepsilon$, the value stored in $b$ is $\keywd{false}$, which means
that any function $f_i$ used will leave the concrete locations storing $x$
and $b$ untouched.

Notice that if the read function also called the call-back, then the
reasoning above would break, as the call-back could modify the value
stored in $x$ because $b$ is $\keywd{true}$.

\section{Conclusions}
\label{sec:conclusions}
We have laid out the basic theory of proof-relevant logical relations
and shown how they can be used to justify nontrivial effect-dependent
program equivalences. We have also shown that proof-relevant logical
relations give direct-style justifications of the Pitts-Stark-Shinwell
equivalences for name generation. For the first time it was possible
to combine effect-dependent program equivalences with hidden
invariants allowing ``silent modifications'' that do not count towards
the ascription of an effect.
Earlier accounts of effect-dependent program equivalences
\cite{DBLP:conf/popl/KammarP12,DBLP:conf/ppdp/BentonKBH09,DBLP:conf/ppdp/BentonKBH07,DBLP:conf/aplas/BentonKHB06,DBLP:conf/icfp/ThamsborgB11}
do not provide such possibilities.

Proof-relevant logical relations or rather the sets $|A\w|$ where $A$
is a semantic type bear a vague relationship with the \emph{model
  variables} \cite{DBLP:journals/spe/CheonLSE05} from ``design by
contract'' \cite{DBLP:journals/computer/Meyer92} and more generally
data refinement \cite{DBLP:books/cu/RoeverE1998}. The commonality is
that we track the semantic behavior of a program part with abstract
functions on some abstracted set of data that may contain additional
information (the ``model''). The difference is that we do not focus on
particular proof methods or specification formalisms but that we
provide a general, sound semantic model for observational equivalence
and program transformation and not merely for functional
correctness. This is possible by the additional, also proof-relevant
part of the semantic equality proofs between the elements of the
models. We also note that our account rigorously supports higher-order
functions, recursion, and dynamic allocation.

Our abstract locations draw upon several ideas from separation logic
\cite{DBLP:conf/lics/Reynolds02}, in particular footprints and the
conditions on rely/guarantee assumptions from
\cite{DBLP:conf/concur/VafeiadisP07}. Intriguingly, we did not need
something resembling the ``frame rule'' although perhaps the
$\Pi$-quantification over larger worlds in function spaces plays its
role.

Pullback-preserving functors and especially the instantiation
\emph{sets of locations} are inspired by FM-sets
\cite{DBLP:journals/fac/GabbayP02} or rather the \emph{Schanuel topos}
to which they are equivalent (see Staton \cite{statonphd} for a
comprehensive account). The instantiations other than \emph{sets of
  locations}, as well as the use of setoids for the ``values'' of
these functors rather than plain sets is original to this work.

\iffull
For a while we worked with groupoids instead of setoids.  At some
point though we found that the required equations between proofs are
needed only to establish other such equations, never in order to prove
something that does not mention them and we thus took the somewhat
bold step to give up all equations between proofs leading us to
setoids. Should we ever want to model dependent types where the index
types are already nontrivial setoids then the passage to groupoids would
become necessary for then, by way of substitution, equality proofs
interfere with actual (semantic) terms. E.g.\ if $p:e\sim e'$ then we
expect a function $A[p]$ from $A[e]$ to $A[e']$.
\fi

We would like to have a semi-formal format that allows one to
integrate semantic arguments with typing and equality derivations more
smoothly. We would also like to allow proof-relevant partial
equivalences in the Heap PER instantiation, which essentially amounts
to the ability to store values with proof-relevant equality. In
particular, this would allow us to model higher-order store with some
layering policy  \cite{DBLP:journals/iandc/Boudol10}. For
unrestricted higher-order store as in
\cite{DBLP:conf/icfp/ThamsborgB11}, but with abstract locations, one
would need to overcome the well-known difficulties with circular
definition of worlds. Step-indexing \cite{DBLP:conf/esop/Ahmed06} is
an option, but we would prefer a domain-theoretic solution. The formal
similarity of our abstract locations with the rely-guarantee formalism
\cite{DBLP:journals/logcom/ColemanJ07,DBLP:conf/concur/VafeiadisP07}
suggests the intriguing possibility of an extension to concurrency.

We also believe that update operations governed by finite state
machines \cite{DBLP:conf/popl/AhmedDR09} can
be modelled as an instance of our framework and thus combined with
effect-dependency. The application of our general framework to effects other
than reading, writing, allocation deserves further investigation.

Indeed, we feel that with the transition to proof-relevance we have
opened a door to a whole new world that hopefully others will
investigate with us.
\iffull

redpajama_set_name: RedPajamaArXiv