% -*- LaTeX -*-
\documentclass{acm}
\usepackage{balance,rawfootnote,amsmath,euler,proof,code,hyperref}

\newif\iftechreport
\techreporttrue

\newtheorem{thm}{Theorem}
\newtheorem{lem}[thm]{Lemma}

\newcommand{\N}[1]{\text{\rm\ttfamily\mdseries{#1}}}
\newcommand{\fprove}{\vdash}
%\newcommand{\fprove}{\mathrel{\vdash{\kern-1ex}\dot{}{\kern.4ex}}}
\newcommand{\fsim}{\mathrel{\sim{\kern-1.2ex}\dot{}{\kern0.7ex}}}
\newcommand{\fsimterm}{\mathrel{\approx{\kern-1.2ex}\dot{}{\kern0.7ex}}}
\newcommand{\df}{\rightharpoonup}
\newcommand{\dfterm}{\Rightarrow}
\newcommand{\deval}{\longrightarrow}
\newcommand{\feval}{\longrightarrow}
%\newcommand{\feval}{\mathrel{\longrightarrow{\kern-2ex}\dot{}{\kern1.35ex}}}
\newcommand{\sidecond}[1]{\quad\mbox{(#1)}}

\newcommand{\Label}[1]{\text{(#1)}}
\newcommand{\Axiom}[2]{{#2} & \Label{#1}}
\newcommand{\Eqn}[3]{{#2} &=& {#3} & \Label{#1}}
\newcommand{\Rule}[3]{\infer{#2}{#3} & \raisebox{1.5ex}{\Label{#1}}}
\newcommand{\Iff}{\quad\text{iff}\quad}
\newcommand{\defeq}{\stackrel{\mathrm{def}}{=}}
\newcommand{\dom}{\mathrm{dom}}

\conferenceinfo{ICFP'04,}{September 19--21, 2004, Snowbird, Utah, USA.}
\CopyrightYear{2004}
\crdata{1-58113-905-5/04/0009}

\title{Translating Dependency into Parametricity}
\author{
Stephen Tse \qquad\qquad Steve Zdancewic \\\\
University of Pennsylvania
\iftechreport \\\\ Technical report: MS-CIS-04-01 \fi
}

\begin{document}
\maketitle

\rawfootnote{Stephen Tse {\tt <stse\@cis.upenn.edu>} and Steve
  Zdancewic {\tt <stevez\@cis.upenn.edu>}.}

\begin{abstract}
  Abadi et al.~introduced the {\em dependency core calculus} (DCC) as
  a unifying framework to study many important program analyses such
  as binding time, information flow, slicing, and function call
  tracking. DCC uses a lattice of monads and a nonstandard typing rule
  for their associated {\em bind} operations to describe the
  dependency of computations in a program.  Abadi et al.~proved a {\em
    noninterference} theorem that establishes the correctness of DCC's
  type system and thus the correctness of the type systems for the
  analyses above.
  
  In this paper, we study the relationship between DCC and the
  Girard-Reynolds polymorphic lambda calculus (System F). We encode
  the recursion-free fragment of DCC into F via a type-directed
  translation. Our main theoretical result is that, following from the
  correctness of the translation, the parametricity theorem for F
  implies the noninterference theorem for DCC.  In addition, the
  translation provides insights into DCC's type system and suggests
  implementation strategies of dependency calculi in polymorphic
  languages.
\end{abstract}

\category{D.3}{Software}{Programming Languages}
\terms{Languages, Security}
\keywords{Dependency, parametricity, noninterference, translation, DCC, information flow, security, monads, polymorphism, lambda calculus, logical relations, protection contexts, Haskell}

\section{Introduction}
\label{sec:intro}
Abadi et al.~introduced the {\em dependency core calculus} (DCC) as
a unifying framework to study many important program analyses such
as binding time, information flow, slicing, and function call
tracking. DCC uses a lattice of monads and a nonstandard typing rule
for their associated {\em bind} operations to describe the
dependency of computations in a program.

For example, information-flow security analyses prevent publicly
visible outputs of a program from revealing information about
confidential inputs~\cite{SM03}.  Consider the program @e@ with
security type as follows:
%
{\[ 
@e : bool_{H} * bool_{L} -> bool_H * bool_{L}@
\]}%
%
Here, the label @H@ indicates {\em high-security} or {\em
  confidential} data and the label @L@ indicates {\em low-security} or {\em
  public} data.  A correct information-flow analysis must ensure that
the low-security output of the function depends only on the
low-security input to the function.  Or, more formally, if we fix the
low-security input to be a constant @e0@, the second output does not
depend on the first input.  This is equivalent to requiring that the
following is a constant function:
%
{\[
@fun x:bool_{H}. prj2 (e <x,e0>) : bool_{H} -> bool_{L}@ \qquad (1)
\]}%
%
If there are no illegal dependencies, @e@ is said to
satisfy {\em noninterference}.  Note that the high-security output of
@e@ may depend on either of the two inputs.

DCC describes dependency analyses by interpreting programs using a
lattice of monads, rather than a single monad as in Moggi's
computational lambda calculus~\cite{Mog91}. The lattice order captures
permissible dependencies: computation interpreted in a monad higher in
the lattice is permitted to depend on data interpreted in a monad
lower in the lattice, but not vice-versa.  Intuitively, computation
higher in the lattice is held abstract with respect to computation
lower in the lattice.  In our example above, the two-point lattice @L
[= H@ suffices: @H@ outputs may depend on @H@ or @L@ inputs, but @L@
outputs may depend only on @L@ inputs.  DCC uses the type constructor
@teel@ to denote the monad corresponding to lattice level @l@, so the
type of @e@ in DCC is:
%
{\[
@e : th bool * tl bool -> th bool * tl bool@
\]}%

The denotational semantics for DCC extensively uses partial
equivalence relations (PERs) indexed by the lattice elements,
suggesting a connection to Reynolds' PER semantics~\cite{Rey83} for
the Girard--Reynolds polymorphic lambda calculus~\cite{Gir72,Rey74}
(System F). It is, therefore, natural to ask whether the parametric
polymorphism in F can express the dependency in DCC.

This paper answers this question affirmatively by giving a
type-directed translation of DCC into F in such that the parametricity
theorem for F implies the correctness of the dependency analysis for
DCC.  

The key idea behind our translation is surprisingly simple.  In DCC,
the type @th bool@ represents a boolean value that is visible only to
@H@ computations (computations that produce data with label @H@).  @L@
computations must treat such a value opaquely and hence cannot
distinguish between @true@ and @false@ at the type @th bool@.  DCC
models this situation via an observation relation that says these two
values are \textit{equal} at @L@ (written @etah true ~l etah false :
th bool@) but not at @H@.  In fact, @~l@ relates every possible pair
of booleans at the type @th bool@, whereas the corresponding @H@
observation relation @~h@ is the \textit{identity} relation.

Our translation simulates DCC's observation relations by encoding @th
bool@ as @ah -> bool@.  An @L@ observer translates to a piece of code
that does not have access to any values of type @ah@, hence any
function of type @ah -> bool@ may not be applied.  Therefore,
in such a context, the two functions @fun x:ah. true@ and @fun
x:ah. false@, which are the translations of @etah true@ and @etah
false@,  are indistinguishable.  

The contributions of this paper are:

\begin{itemize}
\item the development of this translation of DCC into F and proofs of the
  static and dynamic correctness of this translation;
\item a proof of DCC's noninterference derived from F's parametricity
  theorem;
\item a sound extension of DCC's type system suggested by the
  translation into F; and
\item a sketch of how the translation can be used to implement
  DCC--style types in languages with parametric polymorphism.
\end{itemize}

Although the correctness of DCC's type system has been proved
previously~\cite{ABHR99}, the proof method proposed here is
interesting in its own right.  These results not only help to explain
how the nonstandard type system in DCC relates to the well-understood
abstract types in F, but also provide insights on how to make DCC's
type system more expressive.  This translation may also lead to
implementation strategies of dependency calculi in polymorphic
languages. We demonstrate this possibility by giving a Haskell
implementation of the translation for the two-point lattice.

It is known that adding @fix@ to a language weakens the parametricity
theorem~\cite{Wad89,LP96,JV04} and the noninterference
theorem~\cite{HR98,ABHR99} because programs may diverge. For most of
this paper we focus on the terminating fragment of DCC in order to
emphasize the connection between noninterference and parametricity.
Section~\ref{sec:fix} discusses the extension to the translation for
the full DCC with @fix@.

The remainder of this paper is organized as follows.  The next section
introduces the source language of our translation, the dependency core
calculus. Section~\ref{sec:translate} presents the translation and
proves the correctness of the translation. Section~\ref{sec:thm} shows
that the parametricity theorem for F implies the
noninterference theorem for DCC.  Section~\ref{sec:extend} extends
DCC's type system with a protection context to make it more
expressive. The paper concludes with a prototype implementation in
Haskell and a discussion of future and related work.


\begin{figure*}
  \centering
  \[\begin{array}{rclr}
    \Eqn{LP-Unit}{@[[1 >= l]](x:t,m1,m2)@}{@<>@} \\\\

    \Eqn{LP-Pair}{@[[s1 * s2 >= l]](x:t,m1,m2)@}
    {@<[[s1 >= l]](x:t,m1,prj1 m2), [[s2 >= l]](x:t,m1,prj2 m2)>@} \\\\

    \Eqn{LP-Fun}{@[[s1 -> s2 >= l]](x:t,m1,m2)@}
    {@fun x0:s1++. [[s2 >= l]](x:t,m1,m2 x0)@
      \sidecond{fresh @x0@}} \\\\

    \Eqn{LP-Label1}{@[[teel' s >= l]](x:t,m1,m2)@}
    {@fun x0:alphal'. [[s >= l]](x:t,m1,m2 x0)@
      \sidecond{fresh @x0@, @l \not[= l'@}} \\\\

    \Eqn{LP-Label2}{@[[teel' s >= l]](x:t,m1,m2)@}
    {@fun x0:alphal'. (fun x:t. m2 x0) (m1 (kappal'l x0))@ 
      \sidecond{fresh @x0@, @l [= l'@}}
    \end{array}\]
  \caption{Protection translation}
  \label{fig:trans}
\end{figure*}

\section{Dependency core calculus}
\label{sec:dcc}

This section describes the recursion-free fragment of dependency core
calculus (DCC) and explains how dependency information is tracked in
its type system~\cite{ABHR99}. The following grammar defines the syntax for
DCC's contexts, types, values and terms:
%
{\[\begin{array}{rcl}
@Gam@ &::=& @empty | Gam,x:t@ \\
@s@ &::=& @1 | s * s | s + s | s -> s | teel s@ \\
@v@ &::=& @<> | <e,e> | inji e | fun x:s. e | etal e@ \\
@e@ &::=& @v | prji e | case e v v | x | e e | bind x = e in e@
\end{array}\]}%

DCC is a call-by-name, simply-typed lambda calculus with one
additional language construct---a lattice of monads that restrict
dependencies in the program.  Let @lat@ be a lattice of dependency
levels with join @\sqcup@ and order @[=@. We write @latl@ for the set
of lattice labels and @lato@ for the lattice order such that
@lat=(latl,lato)@.  For each element @l \in lat@ there is a monad
@teel@ and its corresponding unit @etal@ and @bind@ operations.

The typing rules for constructs other than the monad operations
(@etal@ and @bind@) are completely standard, so we omit them here. The
following rules prevent low-level computation from depending on
high-level computation:
%
{\[\begin{array}{cr}
\Rule{DT-Prot}{@Gam |- etal e : teel s@}
{@Gam |- e : s@} \\\\

\Rule{DT-Bind}{@Gam |- bind x = e1 in e2 : s2@}
{@Gam |- e1  : teel s1@
  & @Gam,x:s1 |- e2 : s2@
  & @s2 >= l@}
\end{array}\]}%

The @etal e@ operation marks the computation @e@ with the label @l@,
restricting how it interacts with the rest of the program (DT-Prot).
The @bind x = e1 in e2@ operation exposes the computation @e1@ hidden
inside the monad @teel@ to the scope of @e2@ (DT-Bind).  Here,
@e2@ may depend on @e1@, but the results eventually produced by the
entire @bind@ expression must still be protected from computation with
label lower than (or incomparable to) @l@ in the lattice.
Operationally, @bind@ evaluates @e1@ to a value @etal e@ and then
substitutes @e@ for @x@ in @e2@:
%
{\[
@bind x = etal e in e2 --> e2\{e/x\}@
\]}%

Protection rules @s >= l@ (type @s@ protects information at level @l@)
enforce the restrictions on dependencies between computations at
different levels of the lattice:
%
{\[
\begin{array}{crcr}
\Axiom{P-Unit}{@1 >= l@}\\
\\
\Rule{P-Pair}{@s1 * s2 >= l@}
{@s1 >= l@ & @s2 >= l@}
&
\quad
\Rule{P-Label1}{@teel' s >= l@}
{@l \not[= l'@ & @s >= l@} \\
\\
\Rule{P-Fun}{@s1 -> s2 >= l@}
{@s2 >= l@}
&
\Rule{P-Label2}{@teel' s >= l@}
{@l [= l'@}
\end{array}\]}%

No information can be transmitted by a value of type @1@ because there
is only one such value, so computations of type @1@ protect any @l@
(P-Unit).\footnote{Note that if this language permitted diverging
  computations, then information could be transmitted via termination.
  The full DCC calculus includes \emph{lifted} types to distinguish
  between total and partial types.}  Information can be transmitted by
a product only by examining its components, so a product type protects
information when both of its components do (P-Pair). A function will
protect the data as long as the return type of the function protects
the data (P-Fun).

A monad at a \emph{lower} (or incomparable) level of computation does
not protect data at a \emph{higher} monad in the lattice, unless the
contents are already protected at the higher level (P-Label1). On the
other hand, a monad at a \emph{higher} (or equal) level in the lattice
sufficiently protects the results at a lower level (P-Label2).

Note that a sum type, which transmits information via the injection
tags, does not protect data at any level.  To protect a sum in a
@bind@ expression, we must put the sum into a monad. For example, the
program @bind x = eh inj1 <> in x@ is insecure because it leaks the
high-security value @inj1 <>@. The type system will reject the program
as ill-typed because of the typing rule DT-Bind: @x@ has type @1 + s@
but the sum type @1+s@ does not protects information at the high level
(that is, @1+s \not>= H@).

To make examples in the rest of the paper more readable, we define
some syntactic sugar for Boolean values. Let @bool = 1+1@, @true =
inj1 m1@ and @false = m2@, where both @m1@ and @m2@ have type @unit@,
and, for fresh variables @x1@ and @x2@,
%
{\[
@if e then e1 else e2 = case e (fun x1.e1) (fun x2.e2)@
\]}%


\section{DCC to F}
\label{sec:translate}

This section describes a type-directed translation that implements
DCC's monads using parametric polymorphism. The target of the
translation is the polymorphic lambda calculus (System F) extended
with unit, products and sums. The following grammar defines the syntax
for F's type contexts, term contexts, types, values and terms:
%
{\[\begin{array}{rcl}
@Del@ &::=& @empty | Del,alpha@ \\
@Gam@ &::=& @empty | Gam,x:t@ \\
@t@ &::=& @1 | t * t | t + t | t -> t | alpha | all alpha. t@ \\
@u@ &::=& @<> | <m,m> | inji m | fun x:t. m | Fun alpha. m@ \\
@m@ &::=& @u | prji m | case m u u | x | m m | m [t]@
\end{array}\]}%

We use the standard type system and the call-by-name dynamic semantics
for F~\cite{Mit96,Pie02}.  We write its typing judgment as @DG
|> m : t@ and its evaluation as @m1 ->> m2@. 

Although both languages have the same basic features, only DCC has the
dependency constructs (@etal e@ and @bind x = e1 in e2@) while F has
the parametric polymorphism (@Fun alpha.e@ and @e [t]@). The key
observation for the translation is that a function whose input type is
abstract cannot be applied without an argument of the appropriate
type. Hence, if we keep that input type abstract throughout the
translation, such functions can hide expressions in their body and the
type system can ensure that other parts of the program do not depend
on the expressions inside.\footnote{Therefore, we are actually
  translating {\em independency} into parametricity.}


\subsection{Translation}
\label{sec:trans}
Let us start by defining the type translation @s++=t@ and the term
translation @e**=m@. As both DCC and F have the same semantics for the
basic constructs, the following rules simply recurse on the structure
of the terms and do not perform any interesting translation:
%
{\[\begin{array}{rcl}
@1++@ &=& @1@  \\
@(s1 * s2)++@ &=& @s1++ * s2++@ \\
@(s1 + s2)++@ &=& @s1++ + s2++@ \\
@(s1 -> s2)++@ &=& @s1++ -> s2++@ \\
\end{array}\]\[\begin{array}{rcll}
%\\
@<>**@ &=& @<>@ \\
@<e1,e2>**@ &=& @<e1**,e2**>@  \\
@(prji e)**@ &=& @prji e**@ \\
@(inji e)**@ &=& @inji e**@  \\
@(case e v1 v2)**@ &=& @case e** v1** v2**@ \\
@x**@ &=& @x@ \\
@(fun x:s. e)**@ &=& @fun x:s++. e**@ \\
@(e1 e2)**@ &=& @e1** e2**@
\end{array}\]}%

Now, we translate a protection under label @l@ as follows:
%
{\[\begin{array}{rcl}
@(teel s)++@ &=&  @alphal -> s++@ \\
@(etal e)** &=&  fun x:alphal. e**@ \sidecond{fresh @x@}
\end{array}\]}%

We can understand a value of type @alphal@ as a key needed to access
the data @e@. Since @alphal@ is abstract, the only way to access
the data under protection is to apply the function closure to the
right key. We will formalize this noninterference property of DCC in
the next section. A privileged computation that has a key high in the
lattice, however, should be able to use that key to access values
lower in the lattice.  We allow such downgrading of keys via coercion
functions @kappall'@ of type @alphal -> alphal'@. These keys and
coercions are generated fresh from the translation of the lattice
@lat=(latl,lato)@:
%
{\[\begin{array}{rcl}
@latl++ &=& \{ alphal | l \in latl \}@ \\
@lato++ &=& \{ kappall' : alphal -> alphal' | l' [= l \in lato \}@
\end{array}\]}%

The real work is in the translation of @bind@: we have to insert keys
and key coercions such that they satisfy the type translation above.
Recall that the typing rule of @bind@ in DCC is
%
{\[\infer{@Gam |- bind x = e1 in e2 : s2@}
{@Gam |- e1  : teel s1@
  & @Gam,x:s1 |- e2 : s2@
  & @s2 >= l@}
\]}%
%
The type system ensures that a protected expression is eliminated only
if the result of the @bind@ term protects the label (@s2 >= l@).
Therefore, we must translate @bind@ into F terms that have the
corresponding parametric property. Since this property depends on the
protection derivation (@s2 >= l@), our translation is actually
directed by the typing derivation of the term. To simplify the
presentation, we enrich the term @bind x = e1 in e2@ with its typing
information and define the translation on the enriched term as
follows:
\[
@(bind x : s1 = e1 in e2 : s2 >= l)**
= [[s2 >= l]](x:s1++, e1**,e2**)@
\]

Figure~\ref{fig:trans} shows the protection translation @[[s >=
l]](x:t,m1,m2)@, which is defined inductively on the protection
derivation @s >= l@. The first four rules in the figure simply recurse
into components using extensionality. Only the last rule reveals the
value of @e1**@ to @e2**@, which is sound because @e2@ is also a
protection type @teel' s@ with @l [= l'@.  Such dependency of @e2@ on
@e1@ is translated as follows: we coerce a key of type @alphal'@ into
that of @alphal@ by applying the coercion @kappal'l@ and then reveal
the value of @m1 = e1**@ to @m2 = e2**@ by function application. Note
that @x@ of type @s@ is free in @e2@; we keep track of the binding
variable @x:t=x:s++@ and close @m2=e2**@ only after the key is applied
(@fun x:t. m2 x0@).

Let us illustrate the translation rules with an example. Consider the
typing @Gam |- e : s@ in DCC,
\[
@|- fun x1:tl bool. bind x2 = x1 in eh x2 : tl bool -> th bool@
\]

The translations of the type and the enriched term are:
{\[\begin{array}{rcl}
&& @(tl bool -> th bool)++@ \\
&=& @(tl bool)++ -> (th bool)++@ \\
&=& @(al -> bool) -> (ah -> bool)@ \\
\\
&& @(fun x1:tl bool.@ \\
&& @bind x2 : bool = x1 in eh x2 : th bool >= L)**@ \\
&=& @fun x1:al -> bool. [[th bool >= L]](x2:bool++,x1**,(eh x2)**)@ \\
&=& @fun x1:al -> bool. [[th bool >= L]](x2:bool,x1,fun x3:ah.x2)@ \\
&=& @fun x1:al -> bool. fun x0:ah. (fun x2:bool. (fun x3:ah. x2) x0)@ \\
&& @(x1 (khl x0))@
\end{array}\]}%

We also need to translate the lattice to obtain @latl++=ah,al@ and
@lato++=khl:ah->al@ and use them to close the translated term to
obtain the typing @latl++;lato++,Gam++ |- e** : s++@ in
F:\footnote{Actually, as the lattice order is reflexive, we should
  have @lato++=khl:ah->al,khh:ah->ah,kll:al->al@. We leave out the
  last two coercions to simplify the presentation in later sections.}
%
{\[\begin{array}{rcl}
&& @ah,al; khl:ah->al@ \\
&@|>@& 
@fun x1:al -> bool. fun x0:ah. (fun x2:bool. (fun x3:ah. x2) x0)@ \\
&& @(x1 (khl x0))@ \\
&:& @ (al -> bool) -> (ah -> bool)@
\end{array}\]}%

\subsection{Correctness}
In this subsection we prove that the translation is correct with
respect to its static and dynamic semantics. These correctness
theorems are essential in proving the noninterference theorem in the next section.

The static correctness theorem below states that translated terms are
well-typed. We only give proof sketches in this paper; complete proofs
can be found in 
\iftechreport the appendix. 
\else our companion technical report~\cite{TZ03d}. \fi

\begin{thm}[Static correctness]\label{static}
  If @Gam |- e : s@ with @(latl,lato)@, then 
  \[ @latl++;lato++,Gam++ |> e** : s++@ \]
\end{thm}

\begin{proof}
  We prove the theorem by induction on the typing derivation and use
  the following lemma in case of @bind@.
\end{proof}

\begin{lem}
 If @DG |> m1 : alphal ->
    t@ and @DG,x:t |> m2 : s++@, then @DG |> [[s >= l]](x:t,m1,m2) :
    s++@.
\end{lem}

In order to relate the dynamic semantics of the two languages in a
declarative style, we define the following translation relation @v ~>
u : t@ to relate a DCC value @v@ to an F value @u@ at DCC type @t@.  It
is a logical relation~\cite{Mit96} that formalizes
the behavioral equivalence of the dynamic semantics.
%
{\[\begin{array}{cr}
\Axiom{DF-Unit}{@<> ~> <> : 1@} \\\\

\Rule{DF-Pair}{@<e1,e2> ~> <m1,m2> : s1 * s2@}
{@e1 => m1 : s1@ & @e2 => m2 : s2@} \\\\

\Rule{DF-Inj}{@inji e ~> inji m : s1 + s2@}
{@e => m : si@} \\\\

\Rule{DF-Fun}{@v ~> u : s1 -> s2@}
{@all (e => m : s1). v e => u m : s2@} \\\\

\Rule{DF-Prot}{@etal e ~> u : teel s@}
{@all (|> m : t). e => u m : s@} \\\\
\\
\Rule{DF-Term}{@e => m : s@}
{@e -->* v@ & @m ->>* u@ & @v ~> u : s@}
\end{array}\]}%

The last rule defines the translation relation @e => m : s@ for terms
by extending the corresponding relation for values @v ~> u : t@ with
evaluation. We will similarly extend other logical relations for
values to terms by evaluation in later sections.

Note that the relation above is defined for closed types and terms.
Our translated types and terms, however, have free type variables
@alphal@ for the lattice labels and free term variables @kappall'@ for
the lattice order. By the static correctness theorem, we know that
those types and terms are closed under @latl++@ and @lato++@. 

At runtime, we need to link the open term with a well-typed
implementation of the keys and the coercions. We formalize this
linking using term and type substitutions. Let @gam@ denote a
finite map from term variables to values and let @del@ denote a
finite map from type variables to closed types:
%
{\[\begin{array}{rcl}
@gam@ &::=& @empty | x |-> v@ \\
@del@ &::=& @empty | alpha |-> t@
\end{array}\]}%

We define @del(Gam)@ as the pointwise application of @del@ to the
range of @Gam@ such that @(del(Gam))(x)=del(Gam(x))@. Also, we
generalize the definition of the translation relation for values @v
~> u : t@ to term substitutions such that @gam => gam' : del(Gam)@ if
@gam(x) => gam'(x) : del(Gam(x))@ for all @x \in dom(gam)=dom(gam')=dom(Gam)@.
Formally we state the typing requirements of the substitutions as:
%
{\[\begin{array}{rcl}
@gam |= Gam@ &\Iff& @|- gam(x) : Gam(x)@ \\
@del |= Del@ &\Iff& @\dom(del) = Del@
\end{array}\]}%

At last, the dynamic correctness theorem below states that if a term
and a linking are well-typed, then the source and the target terms
have the same dynamic behavior.

\begin{thm}[Dynamic correctness]\label{dynamic}
  If @Gam |- e : s@ with @(latl,lato)@, @del0 |= latl++@, @gam => gam'
  : del0(Gam)@, and @gam0 |= lato++@, then
  \[ @gam(e) => dgz gam'(e**) : s@ \]
\end{thm}

\begin{proof}
  We prove the theorem by induction on the typing derivation and use
  the following lemma in case of @bind@.
\end{proof}

\begin{lem}
  If @DG,x:t |- m2 : s@,
    @del0 |= Del@, @gam0 |= Gam@,\ @m1 m0 ->>* m@\ \ and\ 
    @e2 => m2\{m/x\} : s@, then @e2 => dgz[[s >= l]](x:t,m1,m2)@.
\end{lem}

\section{Theorems}
\label{sec:thm}

This section proves the main theoretical result of the paper: the
parametricity theorem for F implies the noninterference theorem for
DCC. Both theorems are defined in terms of logical equivalence of
the dynamic semantics; therefore, we will use logical relations again
to define related values for DCC and those for F. Then, we come up
with a canonical implementation consisting of substitutions for terms,
types and relations in F. Using these substitutions we can instantiate
parametricity to prove noninterference.

\subsection{Logical equivalences}
\label{sec:logic}
We formalize logical equivalences as logical relations. For
DCC, they extend the identity relations, except that data in a monad
higher in the lattice is opaque at levels lower in the lattice.  We
write @v ~z v' : s@ to denote two related DCC values @v@ and @v'@ at
type @s@ below observation bound @zeta@.  These relations are defined
as follows:
%
{\[\begin{array}{cr}
\Axiom{DR-Unit}{@<> ~z <> : 1@} \\\\

\Rule{DR-Pair}{@<e1,e2> ~z <e1',e2'> : s1 * s2@}
{@e1 ~~z e1' : s1@ & @e2 ~~z e2' : s2@} \\\\

\Rule{DR-Inj}{@inji e ~z inji e' : s1 + s2@}
{@e ~~z e' : si@}\\\\

\Rule{DR-Fun}{@v ~z v' : s1 -> s2@}
{@all (e ~~z e' : s1). v e ~~z v' e' : s2@} \\\\

\Rule{DR-Label1}{@etal e ~z etal e' : teel s@}
{@l \not[= zeta@} \\\\

\Rule{DR-Label2}{@etal e ~z etal e' : teel s@}
{@e ~~z e' : s@ & @l [= zeta@} \\\\
\\
\Rule{DR-Term}{@e ~~z e' : s@}
{@e ->>* v@ & @e' ->>* v'@ & @v ~z v' : s@}
\end{array}\]}%

Except for protection @etal e@, the definitions above are
standard~\cite{Mit96}. The parameter @zeta@ is the context's
observation label, capturing the intuition that the equivalence of two
terms depends on the label of the
observer~\cite{VSI96,HR98,Zda02,SS01,PS02}. For @teel s@, either the
observer's label is below the bound (@l \not[= zeta@) in which case
all values are related (DR-Label1), or two protected terms are
actually related recursively (DR-Label2).

Similarly, we define related values for F.  However, instead of labels
and bounds for DCC, two F values are related at type @t@ under
relation substitution @rho@ (which maps type variables to relations),
written @v ~ v : t | rho@.  These relations are defined as follows:
%
{\[\begin{array}{cr}
\Axiom{FR-Unit}{@<> ~ <> : 1 | rho@} \\\\

\Rule{FR-Pair}{@<m1,m2> ~ <m1',m2'> : t1 * t2 | rho@}
{@m1 ~* m1' : t1 | rho@ & @m2 ~* m2' : t2 | rho@} \\\\

\Rule{FR-Inj}{@inji m ~ inji m' : t1 + t2 | rho@}
{@m ~* m' : ti | rho@} \\\\

\Rule{FR-Fun}{@u ~ u' : t1 -> t2 | rho@}
{@all (m ~* m' : t1 | rho). u m ~* u' m' : t2 | rho@}
\end{array}\]}%
%
{\[\begin{array}{cr}
\Rule{FR-Var}{@u ~ u' : alpha | (rho,alpha|->R)@}
{@(u,u') \in R@} \\\\

\Rule{FR-All}{@u ~ u' : all alpha. t1 | rho@}
{@all (R \in t2 <-> t2').@\hfill 
\\ @u [t2] ~* u' [t2'] : t1 | (rho,alpha|->R)@} \\\\
%{@all (R \in t2 <-> t2'). u [t2] ~* u' [t2'] : t1 | (rho,alpha|->R)@}
\\
\Rule{FR-Term}{@m ~* m' : t | rho@}
{@m ->>* u@ & @m' ->>* u'@ & @u ~ u' : t | rho@}
\end{array}\]}%

The @~*@ relation is the usual logical relation for System
F~\cite{Wad89}. Rule FR-All says that @rho@ maps type variable @alpha@
to \textit{any} relation respecting the types (@R \in t2 <-> t2'@). We
write @t2 <-> t2'@ to denote the set of all binary relations over
values of the types @t2@ and @t2'@. For example, the empty relation
@\emptyset@ and the diagonal relation @\{(<>,<>)\}@ for unit (which we
will use in later sections) are both in the set of all binary
relations over @unit@ and @unit@.

We can also derive the related values at @bool@ in F as follows. The
encoding of Boolean in Section~\ref{sec:dcc} and the rules FR-Unit and
FR-Inj imply the following equivalence:
%
{\[
\infer{@inji m ~ inji m' : 1 + 1 | rho@}
{@m ~* m' : 1 | rho@}
\]}%
%
That is, at @bool@, logical equivalence implies $\beta$-equivalence
modulo the definitions of @true@ and @false@ in Section~\ref{sec:dcc}. In
particular, the definition does not relate the values @true@ and
@false@. The same is true for Booleans in DCC.

\subsection{Parametricity}
System F's parametricity theorem (below) states that, independent of
substitutions for terms, types and relations, a well-typed term is
related to itself. We write @rho \in del <-> del'@ as the pointwise
extension of @R \in t2 <-> t2'@ (which is defined in the last
subsection) such that @rho(alpha) \in del(alpha) <-> del'(alpha)@ for
all @alpha \in dom(rho)=dom(del)=dom(del')@.

\begin{thm}[Parametricity]\label{param}
  If @DG|> m : t@ and @del, del' |= Del@ and @gam ~~
  gam' : Gam | rho@ and @rho \in del <-> del'@, then
  \[ @dg(m) ~~ dg'(m) : t | rho@ \]
\end{thm}

\begin{proof}
  Proofs can be found in standard references~\cite{Rey83,Wad89}. We
  have a full proof in our notation in \iftechreport the appendix \else
  our companion technical report~\cite{TZ03d} \fi and we use the
  following substitution lemma when the induction case is type
  application.
\end{proof}

\begin{lem}
 If @m ~~ m' : t1 | (rho,alpha|->[[t2]]_rho)@, then @m
  ~~ m' : t1\{t2/alpha\} | rho@ where @[[t2]]_rho = \{ (u,u') | u ~
  u' : t2 | rho \}@.
\end{lem}

To motivate our general proof of noninterference from this
parametricity theorem, we demonstrate a simple application using
Wadler's {\em free theorems}~\cite{Wad89}. Recall from the
introduction, that a DCC term of type @th bool -> tl bool@ translates
to a term @m@ of type @(ah -> bool) -> (al -> bool)@.  We use a free
theorem to demonstrate that @m@ is a constant function, which is
required for noninterference.. 

In this instance, we pick the following substitutions for types, terms
and relations:
%
{\[\begin{array}{rcl}
@del0@ &=& @ah |-> 1, al |-> 1@ \\
@gam0@ &=& @khl |-> fun x:1.x@ \\
@rho0@ &=& @ah |-> \emptyset@, @al |-> \{(<>,<>)\}@ 
\end{array}\]}%

By the parametricity theorem and the typing @latl++; lato++ |- m : (ah
-> bool) -> (al -> bool) @, we have
%
{\[
@dgz (m) ~~ dgz (m) : (ah
-> bool) -> (al -> bool) | rho0@
\]}%
%
Applying FR-Fun two times, we have @dgz (m) m1 m2 ~~ dgz (m) m1' m2' :
bool | rho0@ for all @m1 ~~ m1' : ah -> bool | rho0@ and for all @m2
~~ m2 : al | rho0@. Since @rho0@ maps @ah@ to the empty relation, @m1@
and @m1'@ can be different terms (such as @fun x:1.  true@ and @fun
x:1. false@).  Yet @rho0@ maps @al@ to the diagonal relation.  As the
relation @~~@ of related values at @bool@ implies $\beta$-equivalence,
@dgz (m) m1 m2@ is equivalent to @dgz (m) m1' m2'@ despite the
difference in the arguments. In other words, @m@ is a constant
function, or its argument does not interfere with its output.

The key point is that @rho0@ maps the type variable for the high view
to be the empty relation (@ah |-> \emptyset@) and the variable for the
low view to be the diagonal relation on @1@ (@al |->
\{(<>,<>)\}@). Because we translate a protection type @teel s@ into a
function type @alphal -> s++@, we have the complete relation over
@s++@ when @l = H@ and we have the relation defined by @s++@ when @l =
L@. The complete relation formally captures the requirement that the
observer cannot distinguish values in the high view.

Another way to motivate the construction of @rho0@ is the following
two isomorphisms of relations: @\emptyset -> R \cong \top@ and @1 -> R
\cong R@. The former isomorphism says that a function relation from an
empty relation @\emptyset@ to an arbitrary relation @R@ is isomorphic
to the total relation @\top@. Thus, setting @ah |-> \emptyset@ implies
the total relation for the high view, meaning all values are related
(see DR-Label1 in Section~\ref{sec:logic}). On the other hand, the
latter isomorphisms says that a function relation from a diagonal
relation @1@ and an arbitrary relation @R@ is isomorphism to the
relation @R@ itself. Thus, setting @al |-> 1@ implies the relation @R@
itself for the low view, meaning values are related if they are
related recursively (see DR-Label2).

\subsection{Noninterference}
We generalize the approach above to arbitrary lattices and terms to
prove the noninterference theorem.  First, we define an appropriate
implementation of keys based on the lattice @lat@:
%
{\[\begin{array}{rcl}
@[[latl]]_1 &=& \{ alphal |-> 1 | l \in latl \}@ \\
@[[lato]]_1 &=& \{ kappal'l |-> fun x:1.x 
| l [= l' \in lato \}@ \\
@[[latl]]z@ &=& \left\{
\begin{array}{lr}
@alphal |-> \emptyset@ & \mbox{if @l \not[= zeta@} \\
@alphal |-> \{(<>,<>)\}@ & \mbox{if @l [= zeta@}
\end{array}\right.
\end{array}\]}%

This canonical implementation substitutes unit for keys and identity
functions for key coercions. The relation substitution is the diagonal
relation if the observer's label is higher than the data's label, or
the empty relation otherwise. This property of @[[latl]]z@ is critical
in proving Lemma~\ref{relate} and Lemma~\ref{adequacy} below.

The noninterference theorem states that a well-typed term cannot
distinguish substitutions of different values higher than the
observer's bound. We define @gam**@ as @gam**(x) = e**@ iff @gam(x) = e@.

\begin{thm}[Noninterference]\label{ni}
  If @Gam |- e : s@ with @(latl,lato)@ and @gam ~~z gam' : Gam@, then 
  \[ @gam(e) ~~z gam'(e) : s@ \]
\end{thm}

\begin{proof}
  By Theorem~\ref{static} (Static correctness), the translated term is
  well-typed: @latl++;lato++,Gam++ |> e** : s++@. By the definition of
  @del0 = [[latl]]_1@, we have @del0 |= [[latl]]++@. By
  Lemma~\ref{relate} (Relation correctness), the translated
  substitutions are related: @gam0 gam** ~~ gam0 gam'** : lato++,Gam++
  | rho0@. Since @rho0 = [[latl]]z@ is either the empty relation or
  the diagonal relation, @rho0 \in del0 <-> del0@. Then, by
  Theorem~\ref{param} (Parametricity), the translated terms are
  related: @dgz gam**(e**) ~~ dgz gam'**(e**) : s++ | rho0@.
  
  By the definition of @gam0 |= [[lato]]_1@, we have @gam0 |= lato++@.
  The result then follows by Theorem~\ref{dynamic} (Dynamic
  correctness) and Lemma~\ref{adequacy} (Adequacy).
\end{proof}

\begin{lem}[Relation correctness]\label{relate} \
  \begin{enumerate}
  \item If @gam ~~z gam' : Gam@ with @(latl,lato)@ and @gam0 |= lato@,
  then @gam0 gam** ~~ gam0 gam'** : lato++,Gam++ | [[latl]]z@.
  \item If @e ~~z e' : s@ with @(latl,lato)@ and @gam0 |= lato@, then
  @gam0(e**) ~~ gam0(e'**) : s++ | [[latl]]z@.
  \end{enumerate}
\end{lem}

\begin{proof}
  We prove part 2 by induction on the derivation of the related terms
  and thus, by inversion, the derivation of the related values @v ~z
  v' : s@. The important case is @s = teel s0@. When @l \not[=
  zeta@ and thus @[[latl]]z@ is the empty relation, there do not exist
  @m@ and @m'@ such that @m ~* m' : alphal | [[latl]]z@. The
  substituted values are related at the function types @(teel s0)++ =
  alphal -> s0++@ because the premise @all (m ~* m' : alphal |
  [[latl]]z). u m ~* u' m' : s0++ | [[latl]]z@ is vacuously true.
  When @l [= zeta@, we use the induction hypothesis.
\end{proof}

\begin{lem}[Adequacy]\label{adequacy}
  If @e => del0(m) : s@, @e' => del0(m') :s@ with @(latl,lato)@, @del0
  |= latl++@ and @m ~~ m' : s++ | [[latl]]z@, then @e ~~z e' : s@.
\end{lem}

\begin{proof}
  We prove the lemma by induction on the type @s@. When @s = teel s0@
  and @l [= zeta@ and thus @[[latl]]z@ is the diagonal relation, @m
  ~* m' : alphal | [[latl]]z@ for all @m,m'@. Since @(teel s0)++ =
  alphal -> s0++@ and thus @m@ and @m'@ are related at the function
  types, we have @u m ~* u' m' : s++ | [[latl]]z@ given that @m ->>*
  u@ and @m' ->>* u'@.  We can then use induction hypothesis to
  satisfy DR-Label2.
\end{proof}

In the last subsection, we used the parametricity theorem to prove
that a term @m@ of type @(th bool -> tl bool)++=(ah -> bool) -> (al ->
bool)@ is a constant function in F. As an exercise, we want to prove,
directly from the noninterference theorem, that a term @e@ of type @th
bool -> tl bool@ is also a constant function in DCC. Suppose @|- e :
th bool -> tl bool@. By the noninterference theorem, @e ~~z e : th
bool -> tl bool@.  Expanding the definition of DR-Fun, we have @e e2
~~z e e2' : tl bool@ for all @e2 ~~z e2' : th bool@. Since there are
only two points in the lattice, we have @L [= zeta@. Let us pick
@zeta=L@ such that @H \not[= zeta@.  Hence @e2@ and @e2'@ can be
different terms (such as @etal true@ and @etal false@) but still
related by DR-Label1. Yet @e e2@ and @e e2'@ are related by DR-Label2,
implying that both terms evaluate to related Boolean values despite
their arguments. Because the relation @~~@ at type @bool@ implies
$\beta$-equivalence (up to the definition of @bool@), it follows that
@e@ is a constant function.

\section{Extending DCC}
\label{sec:extend}

Having shown that @th bool -> tl bool@ is a constant function, it is
natural to ask: what about functions of other combinations of high
booleans and low booleans? We can easily construct both the constant
functions and the identity functions of types @tl bool -> tl bool@ and
@th bool -> th bool@; therefore, functions of these two types are
unconstrained.

The other interesting case is @tl bool -> th bool@. We claim that,
from the high observer's view (@zeta = H@), @tl bool -> th bool@ is
isomorphic to @bool -> bool@. This isomorphism gives us confidence
that adding labels to a language does not reduce the expressiveness of
the language: if we have a function of type @bool -> bool@, we can
always write an equivalent function of @tl bool -> th bool@ such that
the dependency information is explicit.

But, because of typing, we fail to prove such an isomorphism in DCC.
This section describes how we instead prove the isomorphism in F and,
using insights of the proof, how we extend DCC to type-check the
mediating functions for the isomorphism.

\subsection{Excursion to parametricity}
\label{sec:excursion}

First, we propose the following mediating functions in DCC for the
isomorphism of @s = tl bool -> th bool@ and @bool -> bool@:
%
{\[\begin{array}{rcl}
  @f1@ &:& @(bool -> bool) -> s@ \\
  &=& @fun x1:bool->bool. fun x2:tl bool.@ \\
  && @bind x3 = x2 in eh (x1 x3)@ \\
  %
  @g1@ &:& @s -> (bool -> bool)@ \\
  &=& @fun x4:s. fun x5:bool. bind x6 = x4 (el x5) in x6@
\end{array}\]}%
%

But @g1@ does not type-check. We cannot show @bool >= H@ in
type-checking @x4:s,x5:bool |- bind x6 = x4 (el x5) in x6 : bool@ with
DT-Bind.

Instead we will show that @t@  is isomorphic to
@(bool -> bool)++=bool -> bool@ in F where
%
{\[
@t@ =  @all ah. all al. (ah -> al) -> (al -> bool) -> (ah -> bool)@
\]}%
%
First, we construct these mediating functions in F:
%
{\[\begin{array}{rcl}
  @f2@ &:& @(bool -> bool) -> t@ \\
  &=& @fun x1:bool->bool. Fun ah. Fun al. fun x2:ah->al.@ \\
  && @fun x3:al->bool. fun x4:ah. x1 (x3 (x2 x4))@ \\
  %
  @g2@ &:& @t -> (bool -> bool)@ \\
  &=& @fun x5:t. fun x6:bool. x5 [1] [1]@ \\
  && @(fun x7:1. x7) (fun x8:1. x6) <>@
\end{array}\]}%
%
Now we need to prove that @g2 \circ\, f2@ and @f2 \circ\, g2@ are identity
functions. The first identity @g2 \circ\, f2@ is straightforward from
$\beta\eta$-reductions and we use @=@ to denote
$\beta\eta$-equivalence. For all @|- m0 : bool -> bool@,
%
{\[\begin{array}{rcl}
&& @(g2 \circ\, f2) m0@ \\
% &=& @g2 (f2 m0)@ \\
% &=& @g2 (Fun ah. Fun al. fun x2:ah->al. fun x3:al->bool.@ \\
% && @fun x4:ah. m0 (x3 (x2 x4))@ \\
&=& @fun x6:bool. (fun x2:1->1. fun x3:1->bool. fun x4:1.@ \\
&& @m0 (x3 (x2 x4))) (fun x7:1. x7) (fun x8:1. x6) <>@ \\
% &=& @fun x6:bool. (fun x3:1->bool. fun x4:ah. m0 (x3 x4))@ \\
% && @(fun x8:1. x6) <>@ \\
&=& @fun x6:bool. (fun x4:1. m0 x6) <>@ \\
% &=& @fun x6:bool. m0 x6@ \\
&=& @m0@
\end{array}\]}%

The second identity @f2 \circ\, g2@ requires the parametricity
theorem: for all @|- m1 : all ah. all al.  (ah -> al) -> (ah -> bool)
-> (al -> bool)@:
%
{\[\begin{array}{rcl}
&& @(f2 \circ\, g2) m1@ \\
% &=& @f2 (g2 m1)@ \\
% &=& @f2 (fun x6:bool. m1 [1] [1] (fun x7:1. x7) (fun x8:1. x6) <>)@ \\
&=& @Fun ah. Fun al. fun x2:ah->al. fun x3:al->bool. fun x4:ah.@ \\
&& @(fun x6:bool. m1 [1] [1] (fun x7:1. x7)@ \\
&& @(fun x8:1. x6) <>) (x3 (x2 x4))@ \\
&=& @Fun ah. Fun al. fun x2:ah->al. fun x3:al->bool. fun x4:ah.@ \\
&& @m1 [1] [1] (fun x7:1. x7) (fun x8:1. (x3 (x2 x4))) <>@
\end{array}\]}%

We appear to be stuck at this point: there are no more
$\beta\eta$-reductions to apply because @m1@ is abstract. However,
@m1@ has a polymorphic type @t@ and, by the parametricity theorem,
@m1 ~~ m1 : all ah. all al.  (ah -> al) -> (ah -> bool) -> (al ->
bool) | rho@.  Expanding the definitions of FR-All and FR-Fun
(together with FR-Term) for a few times, we obtain
%
{\[
@m1 [t1] [t2] m2 m3 m4 ~~ m1 [t1'] [t2'] m2' m3' m4' : bool | rho'@
\]}%
as long as the following conditions are satisfied:
%
{\[\begin{array}{rcl}
@rho'@ &=& @rho,ah|->R1,al|->R2@ \\
@R1@ &\in& @t1 <-> t1'@ \\
@R2@ &\in& @t1 <-> t1'@ \\
@m2 ~~ m2'@ &:& @ah -> al | rho'@ \\
@m3 ~~ m3'@ &:& @al -> bool | rho'@ \\
@m4 ~~ m4'@ &:& @ah | rho'@
\end{array}\]}%

We pick the types, relations and terms as follows:
%
{\[\begin{array}{rclrcl}
@t1@ &=& @1@
& @t1'@ &=& @ah@ \\
@t2@ &=& @1@
& @t2'@ &=& @al@ \\
@R1@ &=& @fun x1':1. x4@ &&& \\
@R2@ &=& @fun x2':1. x2 x4@ &&& \\
@m2@ &=& @fun x7:1. x7@
& @m2'@ &=& @x2@ \\
@m3@ &=& @fun x8:1. x3 (x2 x4)@
\quad
& @m3'@ &=& @x3@ \\
@m4@ &=& @<>@
& @m4'@ &=& @x4@ \\
\end{array}\]}%

But we need to check that these definitions satisfy those conditions
above. First, since @R1@ is a function of type @1 -> ah@, we have @R1
\in 1 <-> ah@ (a binary relation of @1@ and @ah@). The same goes for
@R2@ of type @1 -> al@.

Then, we check that @m2 ~~ m2' : ah -> al | rho'@. By FR-Fun, it
is equivalent to check that @m2 m5 ~~ m2' m5' : al | rho'@ for all @m5
~~ m5' : ah@. By FR-Var, @m5' = R1 m5 = x4@ and it is equivalent to
check that @R2 (m2 m5) = m2' m5'@. Indeed, @R2 (m2 m5) = (fun x1':1.
x2 x4) ((fun x7:1.  x7) m5) = x2 x4@ and @m2' m5' = x2 (R1 m5) = x2
x4@.

Similarly, we check that @m3 ~~ m3' : al -> bool | rho'@. For all @m6
~~ m6' : al | rho'@ such that @m6' = R2 m6 = x2 x4@, we have @m3 m6 =
(fun x8:1. x3 (x2 x4)) m6 = x3 (x2 x4)@ and @m3' m6' = x3 (x2 x4)@. At
last, we check that @m4 ~~ m4' : ah | rho'@ which follows from @R1 m4
= x4@ and @m4' = x4@.

Since the relation @~~@ of related values at @bool@ implies
$\beta$-equivalence, the parametricity theorem implies that
%
{\[\begin{array}{rcl}
&& @m1 [1] [1] (fun x7:1. x7) (fun x8:1. (x3 (x2 x4))) <>@ \\
&=&  @m1 [ah] [al] x2 x3 x4@
\end{array}\]}%
%
which we can use to finish the proof:
%
{\[\begin{array}{rcl}
&& @(f2 \circ\, g2) m1@ \\
&=& \cdots \\
% &=& @Fun ah. Fun al. fun x2:ah->al. fun x3:al->bool. fun x4:ah.@ \\
% && @m1 [1] [1] (fun x7:1. x7) (fun x8:1. (x3 (x2 x4))) <>@ \\
&=& @Fun ah. Fun al. fun x2:ah->al. fun x3:al->bool. fun x4:ah.@ \\
&&  @m1 [ah] [al] x2 x3 x4@ \\
&=& @m1@
\end{array}\]}%

\subsection{Protection contexts}
The excursion to F and parametricity shows that our intuition is
right: @tl bool -> th bool@ is isomorphic to @bool -> bool@ (from the
high observer's view) in a richer system like F, even though their
mediating function does not type-check in DCC. Using insights from the
translation, we now show how to extend DCC's type system to allow such
an isomorphism.

From the translation, we observe that the {\em protection context} is
explicit in the typing rule of functions in F but missing in the
typing rule of @bind@ in DCC. In F, protections @etal e@ are
translated into functions and the type system uses the typing context
@Gam@ to keep track of the variable assumptions and thus the
protection assumptions. In DCC, the type system does not make
such protection assumptions of a term.  For example, @eh (bind x = eh true
in x)@ should type-check, because the result of the @bind@ is
protected by @eh@ in the outside context, but this term is not
well-typed in DCC.

Therefore, we propose to extend the typing judgment of DCC to be
@Gam;pi |- e : s@ where @pi\in latl@ is the protection context. This
is similar to the {\em program counter labels} that provide contextual
information found in security-typed languages~\cite{HR98,ZM01,TZ03}.
The function types @s1 -> s2@ now becomes @[pi] s1 -> s2@ to account
for the protection context. The new typing rules are:
%
{\[\begin{array}{c}
\infer{@Gam; pi1 |- fun x:s1. e : [pi2] s1 -> s2@}
{@Gam, x:s1; pi2 |- e : s2@} \\\\

\infer{@Gam; pi1 |- e1 e2 : s2@}
{@Gam; pi1 |- e1 : [pi2] s1 -> s2@
& @Gam; pi1 |- e2 : s1@
& @pi2 [= pi1@} \\\\

\infer{@Gam; pi |- etal e : teel s@}
{@Gam;pi \sqcup l |- e : s@} \\\\

\infer{@Gam; pi |- bind x = e1 in e2 : s2@}
{@Gam; pi |- e1  : teel s1@
  & @Gam,x:s1; pi |- e2 : s2@
  & @pi |- s2 >= l@}
\end{array}\]}%

The other typing rules are essentially the same but now pass around
the protection context. We add the following new protection rules that
make use of the protection context, or call the old rules otherwise:
%
{\[
\begin{array}{cc}
\infer{@pi |- s >= l@}
{@l [= pi@}
\qquad &
\infer{@pi |- s >= l@}
{@s >= l@ & @l \not [= pi@}
\end{array}\]}%

It appears to be straightforward to extend the translation for this
augmented version of DCC by using the following type translation for
functions: @([pi] s1 -> s2)++ = (alpha_pi * s1++) -> s2++@. Protection
contexts are also useful for other types whose values may contain
delayed computations. For example, in call-by-name calculi like DCC,
the protection context of a product type (@[pi] t1 * t2@) expresses
the constraint that a projection of the product can be made only in a
context higher or equal to @pi@. The typing and translation rules for
protection contexts of other types are similar to those for function
types; we do not investigate further here.


\begin{figure*}
\begin{verbatim}
        data H                         ;     data L = Khl H        -- Lattice
        eta :: s -> T l s              ;     eta e = T (\x -> e)   -- Monad injection
        newtype T l s = T (l -> s)     ;     t (T x) = x           -- T constructor/destructor
        
        class Bind l s2 where bind :: T l s1 -> (s1 -> s2) -> s2
        instance Bind l () where                                   -- P-Unit, LP-Unit
          bind m1 m2 = ()                                          
        instance (Bind l s1, Bind l s2) => Bind l (s1, s2) where   -- P-Pair, LP-Pair
          bind m1 m2 = (bind m1 (fst . m2), bind m1 (snd . m2))    
        instance (Bind l s2) => Bind l (s1 -> s2) where            -- P-Fun, LP-Fun
          bind m1 m2 = \x0 -> bind m1 (\x -> m2 x x0)                
        instance (Bind H s) => Bind H (T L s) where                -- P-Label1, LP-Label1 with H </= L
          bind m1 m2 = T (\x0 -> bind m1 (\x -> t (m2 x) x0))     
        
        instance Bind L (T H s) where                              -- P-Label2, LP-Label2 with L <= H
          bind (T m1) m2 = T (\x0 -> t (m2 (m1 (Khl x0))) x0)        
        instance Bind l (T l s) where                              -- P-Label2, LP-Label0, reflexive
          bind (T m1) m2 = T (\x0 -> t (m2 (m1 x0)) x0)              
\end{verbatim}%
  \caption{Prototype implementation in Haskell for the two-point lattice}
  \label{fig:haskell}
\end{figure*}


\subsection{Isomorphism}
Given the modified type system for DCC, we now go back to show the
isomorphism of @s = tl bool -> th bool@ and @bool -> bool@ by proving
that @g1 \circ\, f1@ and @f1 \circ\, g1@ are identity functions from the
high observer's view (@zeta = H@). The technique is similar to proving
the identities of @f2@ and @g2@ using the parametricity theorem in
Section~\ref{sec:excursion}, but instead uses the noninterference
theorem.

The mediating functions now type-check and have the
following types. With the additional constraint @[H]@ on the
protection context of @g1@, the term @bind x6 = x4 (el x5) in x6@
satisfies the new rule above because @H |- bool >= H@.
%
{\[\begin{array}{rcl}
    @f1@ &:& @[L] ([L] bool -> bool) -> ([L] tl bool -> th bool)@ \\
    @g1@ &:& @[H] ([L] tl bool -> th bool) -> ([L] bool -> bool)@
\end{array}\]}%
%

As before, we use $\beta\eta$-reductions in DCC to prove the
identities, using these equivalences:
%
{\[\begin{array}{rcl}
@bind x = etal e in x &=_\beta& e@ \\
@etal (bind x = e in x) &=_\eta& e@
\end{array}\]}%
%
The first identity @g1 \circ\, f1@ is straightforward: for all @|- e0
: [L] bool -> bool@, we have @(g1 \circ\, f1) e0 = fun x5:bool. bind
x6 = eh (e0 x5) in x6 = e0@.

The second identity @f1 \circ\, g1@ requires the noninterference
theorem: for all @|- e1 : [L] tl bool -> th bool@, we have @(f1
\circ\, g1) e1 = fun x2:tl bool.  bind x3 = x2 in e1 (el x3)@. There
are no more $\beta\eta$-reductions to apply because @e1@ is
abstract. But, using the noninterference theorem, we will prove the
following to order to finish the proof:
%
{\[\begin{array}{rcl}
&& @fun x2:tl bool. bind x3 = x2 in e1 (el x3)@ \\
&=& @fun x2:tl bool. e1 x2@
\end{array}\]}%
%

Consider the applications of these two functions with two related
terms. For all @m2 ~~h m2' : tl bool@ such that @m2 -->* el m3@ and
@m2' -->* el m3'@ and @m3 ~~h m3' : bool@, we have @(fun x2:tl
bool. bind x3 = x2 in e1 (el x3)) m2 -->* e1 (el m3)@ and @(fun x2:tl
bool. e1 x2) m3' -->* e1 (el m3')@. By DR-Label2, @el m3 ~~h el m3' :
th bool@.

By noninterference and the typing @|- e1 : tl bool -> th
bool@, we have @e1 ~~h e1 : tl bool -> th bool@. Expanding the
definition of DR-Fun, we have @e1 (el m3) ~~h e1 (el m3') : tl bool@.
Hence, @fun x2:tl bool. bind x3 = x2 in e1 (el x3) ~~h fun x2:tl bool.
e1 x2 : tl bool -> th bool@, which is the $\beta\eta$-equivalence from
the high observer's view.

\section{Discussion}
\label{sec:discuss}
We have shown in this paper that dependency analyses embodied by DCC's
type system can be translated into F's parametricity.  This embedding
uses only a small subset of F---for instance it does not require any
nontrivial use of type abstraction or application.  DCC therefore
appears to be much weaker than F. One possible future direction is to
investigate additional extensions that preserve DCC's spirit while
admitting more of the expressiveness of F. For instance, generating
new labels dynamically may correspond to first-class type abstraction
in F.  This connection is already being explored by Fluet and
Morrisett, who are investigating the relationship between region-based
memory management, Haskell-style monadic effects, and
polymorphism~\cite{FM04}.

\subsection{Haskell implementation}
Another future direction is to use the ideas behind this translation
to provide implementations of dependency analyses in polymorphic
languages. Figure~\ref{fig:haskell} shows a prototype implementation
in Haskell\footnote{We use Glasgow Haskell Compiler (GHC) 6.2 with
  flags {\tt -fglasgow-exts} and {\tt -fallow-undecidable-instances}.}
for DCC with the two-point lattice @L [= H@.  

Abstract datatypes @H@ and @L@ along with the key coercion function
\verb|Khl :: H -> L| encode the lattice. The type of the function 
\verb|eta :: s -> T l s| corresponds to the typing rule DT-Prot in
Section~\ref{sec:dcc}:
%
{\[\begin{array}{cr}
\Rule{DT-Prot}{@Gam |- etal e : teel s@}
{@Gam |- e : s@}
\end{array}\]}%
%
The definitions of the type \verb|newtype T l s = T (l -> s)| and the
function \verb|eta e = T (\x -> e)| correspond to the translation
rule for protection under label @l@ in Section~\ref{sec:trans}:
%
{\[\begin{array}{rcl}
@(teel s)++@ &=&  @alphal -> s++@ \\
@(etal e)** &=&  fun x:alphal. e**@ \sidecond{fresh @x@}
\end{array}\]}%
%
Finally the destructor \verb|t (T x) = x| encodes the evaluation rule
of @bind@:
%
{\[
@bind x = etal e in e2 --> e2\{e/x\}@
\]}%

The last part of the implementation is to use the typeclass @Bind@ to
encapsulate the typing rule DT-Bind and its protection rules @s >= l@
for the @bind@ operations in Section~\ref{sec:dcc}.  Each instance of
the @Bind@ typeclass corresponds to a translation rule in
Figure~\ref{fig:trans}, except that we also have the instance for the
implicit reflexive cases LP-Label0 when @H [= H@ and @L [= L@.

% monomorphism restriction for label inference: 
% e = \x1 ->  bind x1 (\x2 -> eta x2) versus
% e x1 = bind x1 (\x2 -> eta x2)

The example in Section~\ref{sec:trans} type-checks in Haskell:

{\begin{verbatim}
    e :: T L Bool -> T H Bool
    e x1 = bind x1 (\x2 -> eta x2)
\end{verbatim}}
%
On the other hand, if @e@ is constrained to have the type 
\verb|e :: T H Bool -> T L Bool|,
Haskell will correctly report a type error because of the
illegal dependency of a low output on the high input.  If we omit the
type annotation, Haskell can even do {\em label inference}:

{\begin{verbatim} 
    e :: forall s l1 l. 
         (Bind l (T l1 s)) => T l s -> T l1 s
\end{verbatim}}

Unfortunately, this implementation requires $O(n^2)$ typeclass
instances to encode the @bind@ translation for a lattice containing
$n$ labels. We could have factored the lattice edges into two classes,
class @LE@ (@[=@, less than or equal to) and class @GT@ (@\not[=@,
greater than), such that the number of class instances is shifted to
these two classes, and @Bind@ would only have two instances (one for
@LE@ and one for @GT@). This construction still has the same
complexity of class instances and it requires non-standard Haskell
extensions for checking non-overlapping and complementary instances,
but it may be a more modular approach.

It would also be interesting to see whether other clever programming
tricks, such as \textit{phantom types}~\cite{FP02}, could reduce this
overhead.  Another alternative is to use explicit subtyping and
bounded quantification, such as $F_{\mathtt{<:}}$~\cite{Pie02}, which
would simplify the description of the label lattice considerably.

\subsection{Fixpoints and termination}
\label{sec:fix}
It is known that adding @fix@ (and side-effects in general) to System F
weakens the parametricity theorem because programs may
diverge~\cite{Wad89,LP96,JV04}.  A similar phenomenon arises in
noninterference, which may be defined to be termination
sensitive~\cite{HR98,ABHR99}.

This paper focuses on the terminating fragment of DCC, which helps to
emphasize the connection between noninterference and parametricity.
Like the original DCC, we would need to add pointed types and a @fix@
operator to F to account for termination.  We expect that all of the
results presented here carry through to the case where @fix@ is added
to both DCC and F, assuming that noninterference and parametricity are
suitably weakened to account for the possibility of diverging
computations~\cite{JV04}.  However, the translation should be slightly
altered to prevent ``forged'' keys from being used to access protected
data. 

The problem is that having @fix@ in the language allows
arbitrary keys or coercions to be created, because all types are
inhabited. For example, the following term
%
{\[
@fix (fun x:ah. x) : ah@
\]}%
%
can be used to unlock any high-security data. Note that, however, this
term is non-terminating. To prevent such keys from being used by a bad
F context, we can simply force the evaluation of the key by using a
construct similar to @seq@ in Haskell.  Essentially, we need to modify
the translation rules for protection LP-Label1 and LP-Label2 in
Figure~\ref{fig:trans} as follows:

\[\begin{array}{rcl}
  && @[[teel' s >= l]](x:t,m1,m2)@  \hskip15ex\text{where @l \not[= l'@} \\
  &=& @fun x0:alphal'. seq x0 ([[s >= l]](x:t,m1,m2 x0))@
  \\\\

  && @[[teel' s >= l]](x:t,m1,m2)@  \hskip15ex\text{where @l [= l'@} \\
  &=& @fun x0:alphal'. seq x0 ((fun x:t. m2 x0) (m1 (kappal'l x0)))@ 
\end{array}\]

Further investigating the interactions between side effects and
relational parametricity is an important area of ongoing research.

\subsection{Related work}
The ideas behind our encoding of DCC into F are similar to
Sumii and Pierce's work on the cryptographic lambda
calculus~\cite{SP01}.  They use logical relations (and, more recently,
bisimulations~\cite{SP04}) to capture the effects of encryption as an
information-hiding mechanism.  Knowledge of a cryptographic key is
sufficient to reveal the encrypted data.  In this paper, our
translation uses function closures with types of the form @alphal ->
t@ to represent hidden data of type @t@.  Possession of a key of type
@alphal@ allows the computation to obtain the data hidden in the
closure.  Unlike Sumii and Pierce's work, our translation must also
account for DCC's lattice order using key coercions.

Sabelfeld and Sands used PER models to prove noninterference
properties in the context of information-flow security~\cite{SS01}.
Benton uses logical relations to prove program transformations related
to information-flow and dependency correct~\cite{Ben04}.  Both of
these approaches, as we do here, use complete relations to represent
abstract views of data.

Other researchers have studied languages via translation into
F.  For example, Washburn and Weirich~\cite{WW03} use parametric
polymorphism to encode higher-order abstract syntax.  There,
parametricity is also essential to show that the encoding is adequate.

\section{Conclusion}
This paper has shown how to encode the dependency core
calculus, which is useful for modeling many kinds of program analyses,
into System F.  This encoding provides both novel insights into the
relationship between dependency and parametricity and an alternate
proof of DCC's noninterference theorem.  We also give a prototype
implementation of this translation in Haskell.  

\section*{Acknowledgments} The authors thank Eijiro
Sumii, Stephanie Weirich, and the anonymous reviewers for their
comments on drafts of this paper. Stephanie also provided the Haskell
prototype.

This research was supported in part by National Science Foundation
grants CNS-0346939 (\textit{CAREER: Language-based Distributed System
Security}) and CCR-0311204 (\textit{Dynamic Security Policies}).

\balance
\bibliographystyle{plain}
\bibliography{all}

\iftechreport
\onecolumn\appendix

\def\Set#1#2{\expandafter\gdef\csname XX-#1\endcsname{#2}}
\def\Get#1{\csname XX-#1\endcsname}
\newcommand{\Thmx}[2]{\Set{X#1}{#2}\Set{Xa#1}{thm}\Set{Xb#1}{Theorem}}
\newcommand{\Lemx}[2]{\Set{X#1}{#2}\Set{Xa#1}{lem}\Set{Xb#1}{Lemma}}
\newcommand{\Lem}[1]{\begin{lem}[\Get{X#1}]\label{#1-appendix}}
\newcommand{\Thm}[1]{\begin{thm}[\Get{X#1}]\label{#1-appendix}}
\newcommand{\Ref}[1]{\Get{Xb#1}~\ref{#1-appendix} (\Get{X#1})}
\newcommand{\Refx}[1]{\Get{Xb#1}~\ref{#1-appendix}}



\Thmx{static}{Static correctness}
\Lemx{static-bind}{Static correctness for bind}
\Thmx{dynamic}{Dynamic correctness}
\Lemx{dynamic-bind}{Dynamic correctness for bind}
\Lemx{f-subs}{Substitution for parametricity}
\Thmx{param}{Parametricity}
\Thmx{df-subs}{Substitution for translation}
\Lemx{df-subs-bind}{Substitution for bind translation}
\Lemx{relate}{Relation correctness}
\Lemx{adequacy}{Adequacy}
\Lemx{conflu}{Confluence}


\newcommand{\Rx}[1]{\Get{X#1}}
\newcommand{\Rr}[1]{#1: \Rx{#1}}

\newcommand{\Rbegin}[2]{ 
  \[\begin{array}{cl}
  \fbox{#2} & \fbox{#1} \\\\}

\newcommand{\Sbegin}{
  \[\begin{array}{rcll}}

\newcommand{\Ebegin}[2]{
  \[\begin{array}{rcll}
  \fbox{#2} &&& \fbox{#1} \\\\}

\newcommand{\Skip}{&\\&\\}
\newcommand{\End}{\end{array}\]}

\newcommand{\Eqnx}[3]{
  \Set{X#1}{#2 = #3}
  {#2} &=& {#3} & {\text{#1}} \\\\}

\newcommand{\Rulex}[3]{
  \Set{X#1}{\infer{#2}{#3}}
  \Rx{#1} & \raisebox{1.5ex}{\text{#1}} \\\\}

\newcommand{\Axiomx}[2]{
  \Set{X#1}{#2}
  \Rx{#1} & {\text{#1}} \\\\}


\section{Syntax}

This section describes the recursion-free fragment of dependency core
calculus (DCC)~\cite{ABHR99} and Girard-Reynolds polymorphic lambda
calculus (System F)~\cite{Gir72,Rey74}.

The following defines the syntax for 
DCC's types, values, terms, evaluation contexts and lattice.


\Sbegin
@s@ & ::= && \fbox{DCC types} \\
&& @1@ & \text{unit} \\
&& @s * s@ & \text{pair} \\
&& @s + s@ & \text{sum} \\
&& @s -> s@ & \text{function} \\
&& @teel s@ & \text{protection} \\
\\
@v@ & ::= && \fbox{DCC values} \\
&& @<>@ & \text{unit} \\
&& @<e,e>@ & \text{pair} \\
&& @inji e@ & \text{injection} \\
&& @fun x:s. e@ & \text{function} \\
&& @etal e@ & \text{protection} \\
\\
@e@ & ::= && \fbox{DCC terms} \\
&& @v@ & \text{value} \\
&& @case e v v@ & \text{injection} \\
&& @prji e@ & \text{projection} \\
&& @x@ & \text{variable} \\
&& @e e@ & \text{application} \\
&& @bind x = e in e@ & \text{bind} \\
\\
@E@ & ::=
& @[]
| prji E
| case E v v
@ & \fbox{DCC Hole} \\
&& @
| E e
| bind x = E in e@ & \\
\\
@lat@ & ::= & @(latl,lato)@ & \fbox{Lattice} \\
@latl@ & ::= & @empty | latl,l@ & \\
@lato@ & ::= & @empty | lato,l [= l@ & \\
\End

\clearpage
Similarly, the following defines the syntax for
F's types, values, terms and evaluation contexts.

\Sbegin
@t@ & ::= && \fbox{F types} \\
&& @1@ & \text{unit} \\
&& @t * t@ & \text{pair} \\
&& @t + t@ & \text{sum} \\
&& @t -> t@ & \text{function} \\
&& @alpha@ & \text{variable} \\
&& @all alpha. t@ & \text{universal} \\
\\
@u@ & ::= && \fbox{F values} \\
&& @<>@ & \text{unit} \\
&& @<m,m>@ & \text{pair} \\
&& @inji m@ & \text{injection} \\
&& @fun x:t. m@ & \text{function} \\
&& @Fun alpha. m@ & \text{polymorphism} \\
\\
@m@ & ::= && \fbox{F terms} \\
&& @u@ & \text{value} \\
&& @prji m@ & \text{projection} \\
&& @case m u u@ & \text{injection} \\
&& @x@ & \text{variable} \\
&& @m m@ & \text{application} \\
&& @m [t]@ & \text{instantiation} \\
\\
@E@ & ::=
& @[]
| prji E
| case E u u
@ & \fbox{F Hole} \\
&& @
| E m
| u [t]
@ & \\
\End


\clearpage
\section{Semantics}

The following are the typing rules for DCC. The typing rules for
constructs other than the monad operations (@etal@ and @bind@) are
completely standard. The @etal e@ operation marks the computation @e@
with the label @l@, restricting how it interacts with the rest of the
program (DT-Prot). 
The @bind x = e1 in e2@ operation exposes the computation @e1@ hidden
inside the monad @teel@ to the scope of the @e2@ (DT-Bind).  Here,
@e2@ may depend on @e1@, but the results eventually produced by the
entire @bind@ expression must still be protected from computation with
label lower than (or incomparable to) @l@ in the lattice.

\Rbegin{DCC Typing}{@Gam |- e : s@}
\Axiomx{DT-Unit}{@Gam |- <> : 1@}

\Rulex{DT-Pair}{@Gam |- <e1,e2> : s1 * s2@}
{@Gam |- ei : si@}

\Rulex{DT-Prj}{@Gam |- prji e : si@}
{@Gam |- e : s1 * s2@}

\Rulex{DT-Inj}{@Gam |- inji e : s1 + s2@}
{@Gam |- e : si@}

\Rulex{DT-Case}{@Gam |- case e v1 v2 : s@}
{@Gam |- e : s1 + s2@
& @Gam |- vi  : si -> s@}

\Axiomx{DT-Var}{@Gam,x:s |- x:s@}

\Rulex{DT-Fun}{@Gam |- fun x:s1. e : s1 -> s2@}
{@Gam, x:s1 |- e : s2@}

\Rulex{DT-App}{@Gam |- e1 e2 : s2@}
{@Gam |- e1 : s1 -> s2@
& @Gam |- e2 : s1@}

\Rulex{DT-Prot}{@Gam |- etal e : teel s@}
{@Gam |- e : s@}

\Rulex{DT-Bind}{@Gam |- bind x = e1 in e2 : s2@}
{@Gam |- e1  : teel s1@
  & @Gam,x:s1 |- e2 : s2@
  & @s2 >= l@}
\End


\clearpage
Protection rules @s >= l@ (type @s@ protects information at level @l@)
enforce the restrictions on dependencies between computations at
different levels of the lattice.

No information can be transmitted by a value of type @1@ because there
is only one such value, so computations of type @1@ protect any @l@
(P-Unit).\footnote{Note that if this language permitted diverging
  computations, then information could be transmitted via termination.
  The full DCC calculus includes \emph{lifted} types to distinguish
  between total and partial types.}  Information can be transmitted by
a product only by examining its components, so a product type protects
information when both of its components do (P-Pair). A function will
protect the data as long as the return type of the function protects
the data (P-Fun).

A monad at a \emph{lower} (or incomparable) level of computation does
not protect data at a \emph{higher} monad in the lattice, unless the
contents are already protected at the higher level (P-Above). On the
other hand, a monad at a \emph{higher} (or equal) level in the lattice
sufficiently protects the results at a lower level (P-Under).

Note that a sum type, which transmits information via the injection
tags, does not protect data at any level.  To protect a sum in a
@bind@ expression, we must put the sum into a monad. For example, the
insecure program @|- bind x = eh inj1 <> in x@ does not type-check, as
@x@ has type @1 + s@ but @1+t >= H@ is not provable.


\Rbegin{Protection}{@s >= l@}
\Axiomx{P-Unit}{@1 >= l@}

\Rulex{P-Pair}{@s1 * s2 >= l@}
  {@si >= l@}

\Rulex{P-Fun}{@s1 -> s2 >= l@}
  {@s2 >= l@}

\Rulex{P-Above}{@teel' s >= l@}
{@l \not[= l'@ & @s >= l@}

\Rulex{P-Under}{@teel' s >= l@}
{@l [= l'@}
\End


\Rbegin{DCC Evaluation}{@e --> e@}
\Rulex{DE-Hole}{@E[e] --> E[e']@}{@e --> e'@}
\Axiomx{DE-Pair}{@prji <e1,e2> --> ei@}
\Axiomx{DE-Sum}{@case (inji e) v1 v2 --> vi e@}
\Axiomx{DE-Fun}{@(fun x:s. e1) e2 --> e1 \{ e2/x \}@}
\Axiomx{DE-Bind}{@bind x = etal e1 in e2 --> e2\{e1/x\}@}
\End


\clearpage
We use the standard type system and the call-by-name dynamic semantics
for F~\cite{Mit96,Pie02}.

\Rbegin{F Typing}{@Gam |> m : t@}
\Axiomx{FT-Unit}{@DG |> <> : 1@}

\Rulex{FT-Pair}{@DG |> <m1,m2> : t1 * t2@}
{@DG |> mi : ti@}

\Rulex{FT-Prj}{@DG |> prji m : ti@}
{@DG |> m : t1 * t2@}

\Rulex{FT-Inj}{@DG |> inji m : t1 + t2@}
{@DG |> m : ti@}

\Rulex{FT-Case}{@DG |> case m u1 u2 : t@}
{@DG |> m : t1 + t2@
& @DG |> ui  : ti -> t@}

\Axiomx{FT-Var}{@DG,x:t |> x:t@}

\Rulex{FT-Fun}{@DG |> fun x:t1. m : t1 -> t2@}
{@DG, x:t1 |> m : t2@}

\Rulex{FT-App}{@DG |> m1 m2 : t2@}
{@DG |> m1 : t1 -> t2@
& @DG |> m2 : t1@}

\Rulex{FT-All}{@DG |> Fun alpha. m : all alpha. t@}
{@Del,alpha;Gam |> m : t@}

\Rulex{FT-Tapp}{@DG |> m [t2] : t1\{t2/alpha\}@}
{@DG |> m : all alpha. t1@}
\End

\Rbegin{F Evaluation}{@m ->> m@}
\Rulex{FE-Hole}{@E[m] ->> E[m']@}{@m ->> m'@}
\Axiomx{FE-Pair}{@prji <m1,m2> ->> mi@}
\Axiomx{FE-Sum}{@case (inji m) u1 u2 ->> ui m@}
\Axiomx{FE-Fun}{@(fun x:t. m1) m2 ->> m1 \{ m2/x \}@}
\Axiomx{FE-All}{@(Fun alpha. m) [t] ->> m \{ t/alpha \}@}
\End


\clearpage
\section{Translation}

This section describes a type-directed translation that implements
DCC's monads using parametric polymorphism. We also prove that the
translation is correct with respect to its static and dynamic
semantics. These correctness theorems are essential in proving the
noninterference theorem in the next section.

\Ebegin{Translation}{@-**@ \quad @-++@ \quad @[[-]]@}
\Eqnx{L-Label}{@(latl,l)++@}{@latl++,alphal@}
\Eqnx{L-Order}{@(lato,l' [= l)++@}{@lato++,kappall':alphal->alphal'@}
\Eqnx{L-Env}{@(Gam,x:s)++@}{@Gam++,x:s++@}
\Eqnx{L-Subs}{@(gam,x|->e)**@}{@gam**,x|->e**@}
\End


\Ebegin{Type translation}{@s++ = t@}
\Eqnx{LT-Unit}{@1++@}{@1@}

\Eqnx{LT-Pair}{@(s1 * s2)++@}{@s1++ * s2++@}

\Eqnx{LT-Sum}{@(s1 + s2)++@}{@s1++ + s2++@}

\Eqnx{LT-Fun}{@(s1 -> s2)++@}{@s1++ -> s2++@}

\Eqnx{LT-Prot}{@(teel s)++@}{@alphal -> s++@}
\End

\Ebegin{Term translation}{@e** = m@}
\Eqnx{LE-Unit}{@<>**@}{@<>@}

\Eqnx{LE-Pair}{@<e1,e2>**@}{@<e1**,e2**>@}

\Eqnx{LE-Prj}{@(prji e)**@}{@prji e**@}

\Eqnx{LE-Inj}{@(inji e)**@}{@inji e**@}

\Eqnx{LE-Case}{@(case e v1 v2)**@}{@case e** v1** v2**@}

\Eqnx{LE-Var}{@x**@}{@x@}

\Eqnx{LE-Fun}{@(fun x:s. e)**@}{@fun x:s++. e**@}

\Eqnx{LE-App}{@(e1 e2)**@}{@e1** e2**@}

\Eqnx{LE-Prot}{@(etal e)**@}{@fun x:alphal. e**@
\sidecond{fresh @x@}}

\Eqnx{LE-Bind}{@(bind x : s1 = e1 in e2 : s2 >= l)**@}
{@[[s2 >= l]](x:s1++, e1**,e2**)@}
\End


\Ebegin{Protection translation}{@[[s >= l]](x:t,m,m) = m@}
\Eqnx{LP-Unit}{@[[1 >= l]](x:t,m1,m2)@}{@<>@}

\Eqnx{LP-Pair}{@[[s1 * s2 >= l]](x:t,m1,m2)@}
{@<[[s1 >= l]](x:t,m1,prj1 m2), [[s2 >= l]](x:t,m1,prj2 m2)>@}

\Eqnx{LP-Fun}{@[[s1 -> s2 >= l]](x:t,m1,m2)@}
{@fun x0:s1++. [[s2 >= l]](x:t,m1,m2 x0)@
\sidecond{fresh @x0@}}

\Eqnx{LP-Above}{@[[teel' s >= l]](x:t,m1,m2)@}
{@fun x0:alphal'. [[s >= l]](x:t,m1,m2 x0)@
\sidecond{fresh @x0@, @l \not[= l'@}}

\Eqnx{LP-Under}{@[[teel' s >= l]](x:t,m1,m2)@}
{@fun x0:alphal'. (fun x:t. m2 x0) (m1 (kappal'l x0))@ 
\sidecond{fresh @x0@, @l [= l'@}}
\End


\Rbegin{DCC-F values}{@v ~> u : s@}
\Axiomx{DF-Unit}{@<> ~> <> : 1@}

\Rulex{DF-Pair}{@<e1,e2> ~> <m1,m2> : s1 * s2@}
{@ei => mi : si@}

\Rulex{DF-Inj}{@inji e ~> inji m : s1 + s2@}
{@e => m : si@}

\Rulex{DF-Fun}{@v ~> u : s1 -> s2@}
{@all (e => m : s1). v e => u m : s2@}

\Rulex{DF-Prot}{@etal e ~> u : teel s@}
{@all (|> m : t). e => u m : s@}

\Skip
\Rulex{DF-Term}{@e => m : s@}
{@e -->* v@ & @m ->>* u@ & @v ~> u : s@}

\Rulex{DF-Subs}{@(gam,x|->e) => (gam',x|->m) : (Gam,x:s)@}
{@gam => gam' : Gam@ & @e => m : s@}
\End

\Rbegin{Models}{@\cdot |= \cdot@}
\Rulex{M-Subs}{@(gam,x |-> e) |= (Gam,x:s)@}
{@gam |= Gam@ & @Gam |- e:s@}

\Rulex{M-Tsubs}{@(del,alpha|->t) |= (Del,alpha)@}{@del |= Del@}
\End


\Thm{static}
  If @Gam |- e3 : s3@ with @(latl,lato)@, then 
  \[ @latl++;lato++,Gam++ |> e3** : s3++@ \]
\end{thm}

\begin{proof}
  By induction on @Gam |- e3 : s3@:
  \begin{itemize}
  \item \Rr{DT-Unit} with @e3 = <>@ and @s3 = 1@

    By \Rr{LE-Unit}, \Rr{LT-Unit} and
    \Rr{FT-Unit}.
    
  \item \Rr{DT-Pair} with @e3 = <e1,e2>@ and @s3 = s1 * s2@
    
    By \Rr{LE-Pair}, \Rr{LT-Pair}, IH: @latl++;lato++,Gam++ |> ei** :
    si++@, and \Rr{FT-Pair}.
    
  \item \Rr{DT-Prj} with @e3 = prji e@ and @s3 = si@
    
    By \Rr{LE-Prj}, IH: @latl++;lato++,Gam++ |> e** : (s1 * s2)++@,
    \Rr{LT-Pair} and \Rr{FT-Prj}.
    
  \item \Rr{DT-Inj} with @e3 = inji e@ and @s3 = s1 + s2@
    
    By \Rr{LE-Inj}, \Rr{LT-Sum}, IH:
    @latl++;lato++,Gam++ |> e** : si++@, and \Rr{FT-Inj}.
    
  \item \Rr{DT-Case} with @e3 = case e v1 v2@ and @s3 = s@

    By \Rr{LE-Case}, IH: @latl++;lato++,Gam++ |> e** :
    (s1 + s2)++@, IH: @latl++;lato++,Gam++ |> vi** : si++ -> s++@,
    \Rr{LT-Sum} and \Rr{FT-Case}.

  \item \Rr{DT-Var} with @e3 = x@ and @s3 = s@

    By \Rr{LE-Var}, \Rr{L-Env} and \Rr{FT-Var}.
    
  \item \Rr{DT-Fun} with @e3 = fun x:s1. e@ and @s3 = s1 -> s2@

    By \Rr{LE-Fun}, \Rr{LT-Fun}, IH:
    @latl++;lato++,Gam++, x:s++ |> e** : s2++@, and \Rr{FT-Fun}.
    
  \item \Rr{DT-App} with @e3 = e1 e2@ and @s3 = s2@

    By \Rr{LE-App}, IH: @latl++;lato++,Gam++ |> e1** :
    (s1 -> s2)++@, IH: @latl++;lato++,Gam++ |> e2** : s1++@, \Rr{LT-Fun} and
    \Rr{FT-App}.
    
  \item \Rr{DT-Prot} with @e3 = etal e@ and @s3 = teel s@

    By \Rr{LE-Prot}, IH: @latl++;lato++,Gam++ |>
    e** : s++@, the weakening and the freshness of @x@:
    @latl++;lato++,Gam++,x:alphal |> e** : s++@, \Rr{LT-Prot} and
    \Rr{FT-Fun}.
    
  \item \Rr{DT-Bind} with @e3 = bind x = e1 in e2@ and @s3 = s2@

    By \Rr{LE-Bind}, \Rr{LT-Prot}, IH:
    @latl++;lato++,Gam++ |> e1** : (teel s1)++@, IH:
    @latl++;lato++,Gam++,x:s1++ |> e2** : s2++@ and \Ref{static-bind}.
  \end{itemize}
\end{proof}


\Lem{static-bind} 
If @DG |> m1 : alphal -> t@ and @DG,x:t |> m2 : s3++@, then
\[@DG |> [[s3 >= l]](x:t,m1,m2) : s3++@\]
\end{lem}

\begin{proof}
  By induction on @[[s3 >= l]](x:t,m1,m2)@:
  \begin{itemize}
  \item \Rr{LP-Unit} with @s3 = 1@

    By \Rr{FT-Unit} and \Rr{LT-Unit}.
    
  \item \Rr{LP-Pair} with @s3 = s1 * s2@

    By \Rr{LT-Pair} and \Rr{FT-Prj}, we have @DG,x:t
    |> prji m2 : si++@. By IH, @DG |> [[si >= l]](x:t,m1,prji m2) :
    si++@. The result follows by \Rr{FT-Pair}.
  
  \item \Rr{LP-Fun} with @s3 = s1 -> s2@

    By \Rr{LT-Fun}, we have @DG,x:t |> m2 : s1++
    -> s2++@. By \Rr{FT-Var}, we have @DG,x0:s1++ |> x0 : s1++@. By
    weakening, the freshness of @x0@ and \Rr{FT-App}, we have
    @DG,x0:s1++,x:t |> m2 x0 : s2++@. By IH, @DG,x0:s1++ |> [[s2 >=
    l]](x:t,m1,m2 x0) : s2++@. The result follows by \Rr{FT-Fun}.
    
  \item \Rr{LP-Above} with @s3 = teel' s@
    
    By \Rr{LT-Prot}, we have @DG |> m2 : alphal' -> s++@. By
    \Rr{FT-Var}, we have @DG,x0:s++ |> x0 : s++@.  By weakening, the
    freshness of @x0@ and \Rr{FT-App}, we have @DG,x0:alphal',x:t |>
    m2 x0 : s++@. By IH, @DG,x0:alphal' |> [[s >= l]](x:t,m1,m2 x0) :
    s++@.  The result follows by \Rr{FT-Fun}.
    
  \item \Rr{LP-Under} with @s3 = teel' s@

    By \Rr{LT-Prot}, we have @DG |> m2 : alphal'
    -> s++@. By \Rr{L-Order}, we have @DG |> kappal'l : alphal' -> alphal@.

    \[\begin{array}{rcll}
      @DG,x0:alphal' |> x0@ &:& @alphal'@ & \quad\text{by FT-Var} \\
      @DG,x0:alphal' |> kappal'l@ &:& @alphal' -> alphal@ & \quad\text{by
        weakening} \\
      @DG,x0:alphal' |> kappal'l x0@ &:& @alphal@ & \quad\text{by FT-App} \\
      @DG,x0:alphal' |> m1@ &:& @alphal -> t@ & \quad\text{by weakening} \\
      @DG,x0:alphal' |> m1 (kappal'l x0)@ &:& @t@ & \quad\text{by
        FT-App} \\
      @DG,x0:alphal',x:t |> x0@ &:& @alphal'@ & \quad\text{by FT-Var} \\
      @DG,x0:alphal',x:t |> m2@ &:& @alphal' -> s++@ & \quad\text{by weakening}
      \\
      @DG,x0:alphal',x:t |> m2 x0@ &:& @s++@ & \quad\text{by FT-App} \\
      @DG,x0:alphal' |> fun x:t. m2 x0@ &:& @t -> s++@ & \quad\text{by FT-Fun} \\
      @DG,x0:alphal' |> (fun x:t. m2 x0) (m1 (kappal'l
      x0))@ &:& @s++@ & \quad\text{by FT-App} \\
      @DG |> fun x0:alphal'. (fun x:t. m2 x0) (m1 (kappal'l
      x0))@ &:& @alphal' -> s++@ & \quad\text{by FT-Fun} \\
    \end{array}\]       
  \end{itemize}
\end{proof}


\Thm{dynamic} If @Gam |- e3 : s3@ with @(latl,lato)@, @gam => gam' : Gam@,
@del0 |= latl++@ and @gam0 |= lato++@, then
\[ @gam(e3) => dgz gam'(e3**) : s3@ \]
\end{thm}

\begin{proof}
  By induction on @Gam |- e3 : s3@:
  \begin{itemize}
  \item \Rr{DT-Unit} with @e3=<>@ and @s3 = 1@
    
    By \Rr{LE-Unit}, \Rr{DF-Unit} and DF-Term.
    
  \item \Rr{DT-Pair} with @e3=<e1,e2>@ and @s3 = s1*s2@
    
    By \Rr{LE-Prj}, IH: @gam(ei) => dgz gam'(ei**) : si@,
    \Rr{DF-Pair} and DF-Term.
    
  \item \Rr{DT-Prj} with @e3=prji e@ and @s3 = si@

 By \Rr{LE-Pair}. By IH, @gam(e) => dgz
    gam'(e**) : s1 * s2@. Then by the inversion of \Rr{DF-Term} and
    \Rr{DF-Pair}, we have @ei => mi : si@. The result follows by
    \Rr{DE-Pair} and \Rr{FE-Pair}.
    
  \item \Rr{DT-Inj} with @e3=inji e@ and @s3 = s1+s2@

 By \Rr{LE-Inj}, IH: @gam(e) => dgz gam'(e**) :
    si@, and \Rr{DF-Inj} and DF-Term.
    
  \item \Rr{DT-Case} with @e3=case e v1 v2@ and @s3 = s@

 By \Rr{LE-Case}. By IH, @gam(e) => dgz
    gam'(e**) : s1 + s2@ and @gam(vi) => dgz gam'(vi**) : si -> s@.
    Then by the inversion of \Rr{DF-Term} and \Rr{DF-Inj}, we have @e
    => m : si@. The result follows by \Rr{DE-Sum}, \Rr{FE-Sum},
    \Ref{conflu} and the inversion of \Rr{DF-Fun}.
    
  \item \Rr{DT-Var} with @e3=x@ and @s3 = s@
    
    By \Rr{LE-Var} and \Rr{DF-Subs}.
    
  \item \Rr{DT-Fun} with @e3=fun x:s1. e@ and @s3 = s1->s2@
    
    By \Rr{LE-Fun}. Suppose @e2 => m2 : s1@.  By \Rr{DE-Fun}, we have
    @(fun x:s1.  gam(e)) e2 --> gam(e)\{e2/x\}@.  By \Rr{FE-Fun}, we
    have @(fun x:s1++. dgz gam'(e**)) m2 ->> dgz
    gam'(e**)\{m2/x\}@.  Let
    \[ 
    @gam1 = gam, x|->e2@
    \qquad @gam1' = gam', x|->m2@ 
    \] 
    such that @gam1(e)=gam(e)\{e2/x\}@ and @gam1'(e)=gam'(e)\{m2/x\}@.
    By \Rr{M-Subs}, we have @gam1 |= Gam,x:s1@. By IH, @gam1(e) => dgz
    gam1'(e**) : s2@.  The result follows by \Ref{conflu},
    \Rr{DF-Fun} and DF-Term.

  \item \Rr{DT-App} with @e3=e1 e2@ and @s3 = s2@
    
    By \Rr{LE-App}. By IH, @gam(e1) => dgz gam'(e1**) : s1 -> s2@ and
    @gam(e2) => dgz gam'(e2**) : s1@. The result follows by the
    inversion of \Rr{DF-Fun} and by \Rr{DF-Term}.
    
  \item \Rr{DT-Prot} with @e3=etal e@ and @s3 = teel s@
    
    By \Rr{LE-Prot}. Suppose @|- m : t@. By \Rr{FE-Fun} and the
    freshness of @x@, we have @dgz gam'(etal e)** m = (fun
    x:del0(alphal).  dgz gam'(e**)) m ->> dgz gam'(e**)@.  By IH,
    @gam(e) => dgz gam'(e**) : s@. The result follows by \Ref{conflu},
    \Rr{DF-Prot} and DF-Term.
    
  \item \Rr{DT-Bind} with @e3=bind x = e1 in e2@ and @s3 = s2@
    
    By \Rr{LE-Bind}. By IH, @gam(e1) => dgz gam'(e1**) : teel s1@. By
    inversion of DF-Term and of \Rr{DF-Prot}, we have @gam(e1) -->*
    etal e@, @dgz gam'(e1**) -->* u@. By IH, @gam1(e2) => dgz
    gam1'(e2**) : s2@ where
    \[ 
    @gam1 = gam, x|->e@
    \qquad @gam1' = gam', x|->u m@ 
    \] 
    
    The result follows \Ref{conflu}, \Ref{dynamic-bind} and
    \begin{eqnarray*}
      && @gam(bind x = e1 in e2)@ \\
      &=& @bind x = gam(e1) in gam(e2)@ \\
      &@-->*@& @bind x = etal e in gam(e2)@ \\
      &@-->*@& @gam(e2)\{ e / x \}@ \\
      &=& @gam1(e2)@
    \end{eqnarray*}
  \end{itemize}
\end{proof}


\Lem{dynamic-bind} If @DG,x0:t0 |- m4 : s4@,
    @del0 |= Del@, @gam0 |= Gam@, @m3 m ->>* m0@ and
    @e => m4\{m0/x0\} : s4@, then
\[ @e2 => dgz[[s4 >= l]](x:t,m3,m4)@ \]
\end{lem}

\begin{proof}
  By inversion of \Rr{DF-Term} of @e => m4\{m0/x0\} : s4@, and then by
  induction on @s4@ of @v ~> u : s2@ and @[[s4 >= l]](x0:t0,m3,m4)@:
  \begin{itemize}
  \item \Rr{DF-Unit} with @s4 = 1@
    \par\Rr{LP-Unit} 

    By DF-Unit and DF-Term.
    
  \item \Rr{DF-Pair} with @s4 = s1 * s2@
    \par\Rr{LP-Pair}
    
    Since @prji m4\{m0/x0\} ->>* mi@ and
    \[ @(prji m4)\{m0/x0\} = prji (m4 \{m0/x0\})@ \]
    we have @ei => (prji m4)\{m0/x0\}@. By IH, @ei => dgz[[si >=
    l]](x0:t0,m3,prji m4)@. By DF-Pair, @<e1,e2> ~> dgz<[[s1 >=
    l]](x0:t0,m3,prj1 m4), [[s2 >= l]](x0:t0,m3,prj2 m4)>@.  The result
    follows by DF-Term.
    
  \item \Rr{DF-Fun} with @s4 = s1 -> s2@
    \par\Rr{LP-Fun}
    
    Since @m4\{m0/x0\} m ->>* u m@ and
    \[ @(m4 m)\{m0/x0\} = m4\{m0/x0\} m0\{m0/x0\} = m4\{m0/x0\} m@ \]
    we have @v e => (m4 m)\{m0/x0\}@. By IH, @v e => dgz[[s2 >=
    l]](x0:t0,m3,m4 m)@. By DF-Fun, @v ~> fun x0:alphal'.  dgz[[s2 >=
    l]](x0:t0,m3,m4 x0)@.  The result follows by DF-Term.    

  \item \Rr{DF-Prot} with @s4 = teel s@
    \par\Rr{LP-Above}
    
    Since @m4\{m0/x0\} m ->>* u m@ and
    \[ @(m4 m)\{m0/x0\} = m4\{m0/x0\} m0\{m0/x0\} = m4\{m0/x0\} m@ \]
    we have @e => (m4 m)\{m0/x0\}@. By IH, @e => dgz[[s >= l]](x0:t0,m3,m4
    m)@. By DF-Above, @etal e ~> fun x0:alphal'.  dgz[[s >= l]](x0:t0,m3,m4
    x0)@.  The result follows by DF-Term.
    
  \item \Rr{DF-Prot} with @s4 = teel s@
    \par\Rr{LP-Under}
    
    Since @m4\{m0/x0\} m ->>* u m@ and
    \[ @(m4 m)\{m0/x0\} = m4\{m0/x0\} m0\{m0/x0\} = m4\{m0/x0\} m@ \]
    we have @e => (m4 m)\{m0/x0\}@. Since @m3 (kappal'l x0) ->>* fun
    x:t. m0@ and @x@ is fresh, we have @m3 (kappal'l x0) ->>* m0@.
    Since @(fun x:t. m4 m) m0 ->>* (m4 m)\{m0/x0\}@, we have @e => (fun
    x:t. m4 m) (m3 (kappal'l x0))@. By DF-Under, @etal e ~> fun
    x0:alphal'. (fun x:t. m4 x0) (m3 (kappal'l x0))@.  The result follows
    by DF-Term.

  \end{itemize}  
\end{proof}

\Lem{conflu} If @e => m : s@ and @m' ->> m@, then
\[ @e ~> m'@ \]
\end{lem}

\begin{proof}
  By the inversion of \Rr{DF-Term}, the confluence of evaluation (@m'
  ->>* u@), and DF-Term.
\end{proof}


\clearpage
\section{Theorems}

This section gives detailed proofs of theorems and lemmas in the
paper. Both the parametricity and the noninterference theorems are
defined in terms of behavioral equivalence of the dynamic semantics;
therefore, we will first use logical relations to define related
values for DCC and those for F.



\Rbegin{DCC related terms}{@v ~z v : s@}
\Axiomx{DR-Unit}{@<> ~z <> : 1@}

\Rulex{DR-Pair}{@<e1,e2> ~z <e1',e2'> : s1 * s2@}
{@ei ~~z ei' : si@}

\Rulex{DR-Inj}{@inji e ~z inji e' : s1 + s2@}
{@e ~~z e' : si@}

\Rulex{DR-Fun}{@v ~z v' : s1 -> s2@}
{@all (e ~~z e' : s1). v e ~~z v' e' : s2@}

\Rulex{DR-Above}{@etal e ~z etal e' : teel s@}
{@l \not[= zeta@}

\Rulex{DR-Under}{@etal e ~z etal e' : teel s@}
{@e ~~z e' : s@ & @l [= zeta@}

\Skip
\Rulex{DR-Term}{@e ~~z e' : s@}
{@e ->>* v@ & @e' ->>* v'@ & @v ~z v' : s@}

\Rulex{DR-Subs}{@(gam,x|->e) ~~z (gam',x|->e') : (Gam,x:s)@}
{@gam ~~z gam' : Gam@ & @e ~~z e' : s@}
\End


\Rbegin{F related values}{@u ~ u : t | rho@}
\Axiomx{FR-Unit}{@<> ~ <> : 1 | rho@}

\Rulex{FR-Pair}{@<m1,m2> ~ <m1',m2'> : t1 * t2 | rho@}
{@mi ~* mi' : ti | rho@}

\Rulex{FR-Inj}{@inji m ~ inji m' : t1 + t2 | rho@}
{@m ~* m' : ti | rho@}

\Rulex{FR-Fun}{@u ~ u' : t1 -> t2 | rho@}
{@all (m ~* m' : t1 | rho). u m ~* u' m' : t2 | rho@}

\Rulex{FR-Var}{@u ~ u' : alpha | (rho,alpha|->R)@}
{@(u,u') \in R@}

\Rulex{FR-All}{@u ~ u' : all alpha. t1 | rho@} {@all (R \in t2 <-> t2'). u [t2]
  ~* u' [t2'] : t1 | (rho,alpha|->R)@}

\Skip
\Rulex{FR-Term}{@m ~* m' : t | rho@}
{@m ->>* u@ & @m' ->>* u'@ & @u ~ u' : t | rho@}

\Rulex{FR-Subs}{@(gam,x|->m) ~~ (gam',x|->m') : (Gam,x:t) |
  rho@}
{@gam ~~ gam' : Gam | rho@ & @m ~~ m' : t | rho@}

\Rulex{F-Rsubs}{@(rho,alpha|->R) \in (del,alpha|->t) <->
  (del',alpha|->t')@}
{@rho \in del <-> del'@ & @R \in t <-> t'@}

\Rulex{F-Rel}{@(u,u') \in [[t]]_rho@}
{@u ~ u' : t | rho@}
\End

\[\begin{array}{rcll}
\Eqnx{LL-Unit}{@[[ latl,l ]]_1@}
{@[[latl]]_1, alphal |-> 1@}

\Eqnx{LO-Unit}{@[[ lato,l [= l' ]]_1@}
{@[[lato]]_1, kappal'l |-> fun x:1.x@}

\Eqnx{L-Above}{@[[ latl,l ]]z@}
{@[[latl]]z, alphal |-> \emptyset@
\sidecond{@l \not[= zeta@}}

\Eqnx{L-Under}{@[[ latl,l ]]z@}
{@[[latl]]z, alphal |-> [[1]]_.@
\sidecond{@l [= zeta@}}
\End


\Thm{param}\
If @DG|> m3 : t3@ and @del, del' |= Del@ and @gam ~~
gam' : Gam | rho@ and @rho \in del <-> del'@, then
\[ @dg(m3) ~~ dg'(m3) : t3 | rho@ \]
\end{thm}

\begin{proof}
  By induction on @DG|> m3 : t3@:
  \begin{itemize}
  \item \Rr{FT-Unit} with @m3 = <>@ and @t3 = 1@

    By \Rr{FR-Unit} and FR-Term because @dg(<>) =
    dg'(<>) = <>@.

  \item \Rr{FT-Pair} with @m3 = <m1,m2>@ and @t3 = t1 * t2@

    By IH and \Rr{FR-Pair} and FR-Term.
    
  \item \Rr{FT-Prj} with @m3 = prji m@ and @t3 = ti@
    
    By IH, the inversion of of FR-Term, the inversion of \Rr{FR-Pair},
    and \Rr{FE-Pair}.

  \item \Rr{FT-Inj} with @m3 = inji m@ and @t3 = t1 + t2@

    By IH and \Rr{FR-Inj} and FR-Term.
    
  \item \Rr{FT-Case} with @m3 = case m u1 u2@ and @t3 = t@
    
    By IH, the inversion of FR-Term, the inversion of \Rr{FR-Inj}, the
    inversion of \Rr{FR-Fun}, and \Rr{FE-Sum}.

  \item \Rr{FT-Var} with @m3 = x@ and @t3 = t@

    By the inversion of \Rr{FR-Subs}.
    
  \item \Rr{FT-Fun} with @m3 = fun x:t1. m@ and @t3 = t1 -> t2@
    
    Suppose @m ~* m' : t1 | rho@. By \Rr{FE-Fun}, we have @(fun
    x:t1. dg(m3)) m ->> dg(m3)\{m/x\}@ and @(fun x:t1. dg'(m3)) m'
    ->> dg'(m3)\{m'/x\}@. Let
    \[ 
    @gam1 = gam, x|->m@
    \qquad @gam1' = gam', x|->m'@ 
    \] 
    such that @gam1(m3) = gam(m3)\{m/x\}@ and @gam1'(m3) =
    gam'(m3)\{m'/x\}@.  By IH, @del gam1(m3) ~~ del' gam1(m3) : t2 |
    rho@. The result follows by \Rr{FR-Fun} and FR-Term.
    
  \item \Rr{FT-App} with @m3 = m1 m2@ and @t3 = t2@

    By IH, @dg(m1) ~~ dg'(m1) : t1 -> t2 | rho@
    and @dg(m2) ~~ dg'(m2) : t1 | rho@. The result follows by the
    inversion of FR-Term and the inversion of \Rr{FR-Fun}.
    
  \item \Rr{FT-All} with @e3 = Fun alpha. m@ and @m3 = all alpha. t@
    
    Suppose @R \in t2 <-> t2'@. By \Rr{FE-All}, we
    have @(Fun alpha. dg(m3)) [t2] ->> dg(m3)\{t2/alpha\}@ and @(Fun
    alpha. dg'(m3)) [t2'] ->> dg'(m3)\{t2'/alpha\}@. Let
    \[ 
    @del1 = del, alpha|->t2@
    \qquad @del1' = del', alpha|->t2'@
    \qquad @rho1 = rho, alpha|->R@
    \] 
    such that @del1 gam(m3) = dg(m3)\{t2/alpha\}@ and
    @del1' gam'(m3) = del' gam'(m3)\{t2'/alpha\}@.  By IH,
    @del1 gam(m3) ~~ del1' gam'(m3) : t | rho1@. The result
    follows by \Rr{FR-All} and FR-Term.
    
  \item \Rr{FT-Tapp} with @e3 = m [t2]@ and @t3 = t1\{t2/alpha\}@

    By IH, @dg(m1) ~~ dg'(m1) : all alpha.  t1 |
    rho@. By the inversion of \Rr{FR-Term}, we have @dg(m) ->>* u@,
    @dg'(m1) ->>* u'@ and @u ~ u' : all alpha. t1 | rho@. Let
    @R=[[t2]]_rho@. By the inversion of \Rr{F-Rsubs}, we have @R\in
    del(t2)<-> del'(t2)@. By the inversion of \Rr{FR-All}, we have @u
    [del(t2)] ~* u' [del'(t2)] : t1 | (rho,alpha|->[[t2]]_rho)@. The
    result follows by \Ref{f-subs}.
  \end{itemize}    
\end{proof}


\Lem{f-subs}\
If @m ~~ m' : t3 | (rho,alpha4|->[[t4]]_rho)@, then 
\[ @m ~~ m' : t3\{t4/alpha4\} | rho@ \]
\end{lem}

\begin{proof}
  By the inversion of \Rr{FR-Term} and by induction on @u ~ u' : t3 |
  (rho,alpha4|->[[t4]]_rho)@:
  \begin{itemize}
  \item \Rr{FR-Unit} with @u = <>@ and @t3 = 1@

    By FR-Unit and FR-Term because
    @1\{t4/alpha4\} = 1@.

  \item \Rr{FR-Pair} with @u = <m1,m2>@ and @t3 = t1 * t2@

    By IH, FR-Pair and FR-Term.
                                                    
  \item \Rr{FR-Inj} with @u = inji m@ and @t3 = t1 + t3@

    By IH, FR-Inj and FR-Term.  
                                                    
  \item \Rr{FR-Fun} with @t3 = t1 -> t2@

    By IH, FR-Fun and FR-Term.  
                                                    
  \item \Rr{FR-Var} and @t3 = alpha = alpha4@
        
    By the inversion of \Rr{F-Rel} and FR-Term because @alpha\{t4/alpha4\} = t4@.

  \item \Rr{FR-Var} and @t3 = alpha != alpha4@

    By FR-Var and FR-Term because @alpha\{t4/alpha4\} = alpha@.
    
  \item \Rr{FR-All} with @t3 = all alpha. t1@
    
    Suppose @R \in t3 <-> t3'@. We have @u [t3] ~*
    u' [t3'] : t3 | (rho,alpha4|->[[t4]]_rho,alpha|->R)@. By IH, @u
    [t3] ~* u' [t3'] : t3\{t4/alpha4\} | (rho,alpha|->R)@.  The result
    follows by FR-All and FR-Term because @(all alpha. t3)\{t4/alpha4\}
    = all alpha. t3\{t4/alpha4\}@.
  \end{itemize}
\end{proof}


\Lem{relate} \
\begin{enumerate}
\item If @gam ~~z gam' : Gam@ with @(latl,lato)@ and @gam0 |= lato++@,
  then @gam0 gam** ~~ gam0 gam'** : lato++,Gam++ | [[latl]]z@.
\item If @e3 ~~z e3' : s3@ with @(latl,lato)@ and @gam0 |= lato++@, then
  @gam0(e3**) ~~ gam0(e3'**) : s3++ | [[latl]]z@.
\end{enumerate}
\end{lem}

\begin{proof}
  We prove Part 1 by induction on \Rr{DR-Subs}, Part 2, \Rr{L-Subs} and
  \Rr{FR-Subs}.
  
  We prove Part 2 as follows: By the inversion of \Rr{DR-Term} and by
  induction on @v ~z v' : s@:
  \begin{itemize}
  \item \Rr{DR-Unit} with @v = <>@ and @s3 = 1@

    \par By LE-Unit, LT-Unit, FR-Unit and FR-Term.

  \item \Rr{DR-Pair} with @v = <e1,e2>@ and @s3 = s1 * s2@

    By LE-Pair, LT-Pair, IH, FR-Prj and FR-Term.

  \item \Rr{DR-Inj} with @v = inji e@ and @s3 = s1 + s2@

    By LE-Case, LT-Sum, IH, FR-Inj and FR-Term.

  \item \Rr{DR-Fun} with @s3 = s1 + s2@

    By LE-Fun, LT-Fun, IH, FR-Fun and FR-Term.
    
  \item \Rr{DR-Above} with @v = etal e@ and @s3 = teel s@
    
    By \Rr{LE-Prot} and \Rr{LT-Prot}. By \Rr{L-Above} and \Rr{FR-Var},
    there do not exist @m@ and @m'@ such that @m ~* m' : alphal |
    [[latl]]z@. The result follows by \Rr{FR-Fun} because the premise
    is vacuously true.
    
  \item \Rr{DR-Under} with @v = etal e@ and @s3 = teel s@
    
    By \Rr{LE-Prot}, \Rr{LT-Prot} and \Rr{L-Under}.  Suppose @m ~*
    m' : alphal | [[latl]]z@.  By \Rr{FE-Fun} and the freshness of @x@,
    we have @gam0(etal e)** m = (fun x:alphal. gam0(e**)) m -->
    gam0(e**)@ and @gam0(etal e')** m = (fun x:alphal.  gam0(e'**)) m
    --> gam0(e'**)@.  By IH, @gam0(e**) ~~ gam0(e'**) : s++ |
    [[latl]]z@.  The result follows by \Rr{FR-Fun}.
  \end{itemize}  
\end{proof}


\Lem{adequacy} If @e3 => del0(m3) : s3@, @e3' => del0(m3') :s3@ with
@(latl,lato)@, @del0 |= latl++@ and @m3 ~~ m3' : s3++ | [[latl]]z@,
then
\[ @e3 ~~z e3' : s3@ \]
\end{lem}

\begin{proof}
  By the inversion of \Rr{DF-Term} and \Rr{FR-Term}, then by induction
  on @s3@ of @s3++ = t3@, @v ~> u : s3@, @v' ~> u' : s3@ and @u ~ u' : s3++
  | [[latl]]z@:
  \begin{itemize}
  \item \Rr{LT-Unit}, DF-Unit and FR-Unit with @s3=1@

    By DR-Unit and DR-Term.

  \item \Rr{LT-Pair}, DF-Pair and FR-Pair with @s3=s1*s2@
    
    By IH, DR-Pair and DR-Term.

  \item \Rr{LT-Sum}, DF-Inj and FR-Inj with @s3=s1+s2@
    
    By IH, DR-Inj and DR-Term.

  \item \Rr{LT-Fun} with @s3=s1->s2@
    \par\Rr{DF-Fun}\par\Rr{FR-Fun}
    
    Suppose @e ~~z e' : s1@. Let @gam0 = [[lato]]_1@. By
    \Ref{dynamic}, @e => dgz (e**) : s1@ and @e' => dgz (e'**) : s1@.
    Let @m = gam0 (e**)@ and @m' = gam0(e'**)@.  By \Ref{relate}, @m
    ~~ m' : s1++ | [[latl]]z@. By the inversion of DF-Fun, @v e => u m
    : s2@ and @v' e' => u' m' : s2@ because @v@ and @v'@ are related
    at function type @s1 -> s2@ by assumption. By the inversion of
    FR-Fun, @u m ~~ u' m' : s2++ | [[latl]]z@ because @u@ and
    @u'@ are related at @s1++ -> s2++@. By IH, @v e ~~z v' e' : s2@.
    The result follows by \Rr{DR-Fun} and DR-Term.
    
  \item \Rr{LT-Prot} with @v=etal e@ and @s3=teel s@
    \par\Rr{DF-Prot}\par\Rr{FR-Fun}
    
    If @l \not[= zeta@, the result follows by \Rr{DR-Above} and
    DR-Term.
    
    Suppose @l [= zeta@. By \Rr{L-Under} and \Rr{FR-Var}, we have @m2
    ~* m2' : alphal | [[latl]]z@ for all @m2,m2'@ because the relation
    is total. This implies @u m2 ~* u' m2' : s++ | [[latl]]z@ as @u@
    and @u'@ are related at a function type @alphal -> s++@ by
    assumption. By the inversion of DF-Prot, @e3 => u m2 : s@ and @e3'
    => u' m2' : s@.  The result follows by IH, \Rr{DR-Under} and
    DR-Term.
  \end{itemize}
\end{proof}
\fi

\end{document}