\section{ML5}
\label{ml5}
\subsection{A modal logic for distributed computing}

We present ML5, a high level programming language for distributed computing.

In distributed computing, a program execution takes place at different
locations, but these locations can have different capabilities.
To address this difficulty, ML5 propose a solution by enriching the ML type system with locations
\cite{murphy2008modal,murphy2007ml5}.

With functional languages, types systems are strongly connected with
logic.
With the Curry-Howard isomorphism we interpret types as propositions
and programs become proofs of the propositions corresponding to the 
types they inhabit.

To introduce a type system with a notion of location, modal logic
was chosen, because it allows reasoning from different point of view.


\subsubsection{IS5}

IS5 is the modal logic on which on which ML5 type system is based.
The logic we present here is in fact a particular case of this logic.

\begin{figure}[h]
  $$ A , B ::= \Box A \, | \, \Diamond A \, | \,  A \supset B  \, | \, A \, at \, w \, | 
  A \vee B \, | \,  A \wedge B \, | \, p$$
\caption{Syntax of propositions in the IS5 logic}
\end{figure}

In this logic judgements take the form
$$ \Gamma \vdash A @ w $$
meaning that under the assumption $\Gamma$,  $A$ is true 
at the world $w$.
Hypothesis in $\Gamma$ take the form $B @ w'$.

The rules of this logic are given in figure \ref{is5}
The connectives $\vee$ , $\wedge$ and $\supset$ (for implication) have the
the same meaning than in non-modal intuitionistic logic when reasoning at
the same location .
For instance if we know $A @ w$ and $B @ w$ then we can conclude
$A \wedge B @ w$.

$\Box A$ means that A is true in all world, therefore if we know
$\Box A @ w$, we can conclude $ A @ w'$ . 
In order to prove $\Box A$ we need to prove $A @ \omega$, without
knowing anything about the world $\omega$.

$\Diamond A $ means that A is true at some world. 
To prove $\Diamond A$ we only have to give a proof of it at 
one location.
What we can conclude from it, is what we can conclude of 
knowing $A @ \omega$ without knowing anything about $\omega$.

$ A \, at \, w$ is the internalization in the logic of the judgement $A @ w$.

\begin{figure}[h]
% rules for ``and''
$$
\inferrule* [Left=\textsc{$\wedge$ I}]
{\Gamma \vdash A @ \textsc w \\ \Gamma \vdash B @ \textsc w }
{\Gamma \vdash A \wedge B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\wedge \textsc E_1$}]
{\Gamma \vdash A \wedge B @ \textsc w }
{\Gamma \vdash A @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\wedge \textsc E_2$}]
{\Gamma \vdash A \wedge B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

% rules for ``or''
$$
\inferrule* [Left=\textsc{$\vee \textsc I_1$}]
{\Gamma \vdash A @ \textsc w}
{\Gamma \vdash A \vee B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\vee \textsc I_2$}]
{\Gamma \vdash B @ \textsc w}
{\Gamma \vdash A \vee B @ \textsc w }
$$

$$
\inferrule* [Left=\textsc{$\vee \textsc E$}]
{\Gamma \vdash A \vee B @ \textsc w' \\ 
  \Gamma , A @ \textsc w' \vdash  C @ \textsc w \\
  \Gamma , B @ \textsc w' \vdash C @ \textsc w}
{\Gamma \vdash C @ \textsc w}
$$

% rules for implication
$$
\inferrule* [Left=\textsc{$\supset \textsc I$}]
{\Gamma, A @ \textsc w \vdash B @ \textsc w }
{\Gamma \vdash A \supset B @ \textsc w }
\hspace{4em}
\inferrule* [Left=\textsc{$\supset \textsc E$}]
{\Gamma \vdash A \supset B @ \textsc w \\ \Gamma \vdash A @ w}
{\Gamma \vdash B @ \textsc w }
$$

$$
\inferrule* [Left=\textsc{atI}]
{\Gamma \vdash A @ \textsc w}
{\Gamma \vdash A \, at \, \textsc w @ \textsc w'}
\hspace{4em}
\inferrule* [Left=\textsc{atE}]
{\Gamma \vdash A \, at \, \textsc w'' @ \textsc w' \\ \Gamma, A @ \textsc w'' \vdash B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ $ \Box $ I}]
{\Gamma , \omega \hspace{0.5em} world \vdash A  @ \omega}
{\Gamma \vdash \Box A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Box $ E}]
{\Gamma \vdash \Box A @ \textsc w}
{\Gamma \vdash A @ \textsc w'}
$$


$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash A @ \textsc w'}
{\Gamma \vdash \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash \Diamond A @ \textsc w' \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash B @ \textsc w}
{\Gamma \vdash B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ hyp}]
{\\}
{\Gamma, A @ \textsc w, \Gamma' \vdash A @ \textsc w}
$$

\caption{IS5}
\label{is5} 
\end{figure} 


\subsubsection{Lambda 5 natural deduction}

Lambda 5 is the lambda calculus corresponding to proof terms
of the IS5 logic.
In order to make location changes explicit, a new rule is added, 
it's the $\textsc{get}$ rule.
Therefore the logic presented in figure \ref{fig:lambda5} is different
from IS5 but remains equivalent.

Judgments now take the form 
$$
\Gamma \vdash M : A @ \textsc w
$$
meaning that $M$ is a proof of $A @ \textsc w$ under the hypothesis $\Gamma$.


We constrain the rules to act locally and add the $\textsc{get}$ rule, we give here 
a fragment of the calculus , some of the rules are not mentioned as they
are not modified.

\begin{figure}[h]
$$
\inferrule* [Left=\textsc{atI}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{hold} M : A \, at \, \textsc w @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{atE}]
{\Gamma \vdash M : A \, at \, \textsc w' @ \textsc w \\ 
  \Gamma, A @ \textsc w' \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{leta} M \,in\, N : B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ $ \Box $ I}]
{\Gamma , \omega \hspace{0.5em} world \vdash M : A  @ \omega}
{\Gamma \vdash \textbf{box} M : \Box A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Box $ E}]
{\Gamma \vdash M : \Box A @ \textsc w}
{\Gamma \vdash \textbf{unbox} M : A @ \textsc w}
$$


$$
\inferrule* [Left=\textsc{ $ \Diamond $ I}]
{\Gamma \vdash M : A @ \textsc w}
{\Gamma \vdash \textbf{here} M : \Diamond A @ \textsc w}
\hspace{4em}
\inferrule* [Left=\textsc{ $ \Diamond $ E}]
{\Gamma \vdash M : \Diamond A @ \textsc w' \\
 \Gamma , \omega \hspace{0.5em} world , A @ \omega \vdash N : B @ \textsc w}
{\Gamma \vdash \textbf{letd} \omega , x = M  \,in\, N : B @ \textsc w}
$$

$$
\inferrule* [Left=\textsc{ get }]
{A \textbf{mobile} \\
 \Gamma \vdash M : A @ \textsc w'}
{\Gamma \vdash \textbf{get} [w'] M : A @ \textsc w}
$$

\caption{Lambda 5 natural deduction}
\label{fig:lambda5}
\end{figure} 

We restrict the $\textbf {get} $ construct to $\textbf {mobile}$ types.
These are types of the values that can be safely communicated between worlds.

\begin{figure}[h]
$$
\inferrule{ \\ }{\Box \textbf{ mobile}}
\hspace{4em} \inferrule{ \\ }{\Diamond \textbf {mobile}}
$$

$$
\inferrule{A \textbf{ mobile} \\ B \textbf {mobile} } {A \vee B \textbf{ mobile}}
\hspace{4em}  \inferrule{A \textbf{ mobile} \\ B \textbf {mobile} } {A \wedge B \textbf{ mobile}}
$$

$$
\inferrule{ \\ }{A \, at \, \textsc w \textbf{ mobile} }
$$
\caption{The \textit{mobile} judgment }
\end{figure}


\subsection{Validity}

In general, a large amount of the code written in an
application is not particular to any location, 
so a validity judgment is added.
This judgment takes the form $ u \sim A $ 
meaning that u can have the type A at any world.
The way we introduce validity judgment in a program 
is by using the $\textbf {put}$ declaration.
This judgment is internalized in the logic with
the $\{\}$ (``shamrock'') modality.
Type inference make declaration 
valid when possible.


\subsection{Implementation}
\subsubsection*{A compiler : ml5pgh}

ml5pgh is an implementation for an ML5 compiler. 
It's specialized for web applications involving a web browser and 
a HTTP server. The code produced consists of Javascript for the 
web browser side and bytecode for the server side. 
Javascript can be executed by most web browsers , but for the 
bytecode produced, a specific server which can interpret the
bytecode has been implemented.
Although it can only produce this two kind of code, most of
the step in the compiler are independent from this particular
setting, and in order to add new output languages ,
only the step of code generation would have to be added.

\subsubsection*{Web Features}

ML5 can be extended by external functions.
On the server side we typically have a database library to access
some file that we can read and write.
On the browser side we can use every Javascript primitive.
In particular a library manipulating DOM objects is furnished,
DOM (Document Object Mode) is a standard model for representing 
HTML or XML.
This allows ML5 programs to dynamically modify the structure 
of the page they are executed in, it also gives other usefull
capabilities like access to cookies or redirection to another website.


\subsection{Example}

\begin{figure}[h]
\caption{A piece of ML5 source code}
\label{fig:ml5code}
\begin{verbatim}
put checked_sig = from server get hold (checksig sig)

val _ = 
  from server get 
    let leta cs = checked_sig
    in 
      case cs of 
        NONE => from home get setstring ([you are not logged in])
      | (SOME log) => from home get setstring ([ OK ])
    end

\end{verbatim}
\end{figure}

We present an example in figure \ref{fig:ml5code}, which illustrates some
ML5 primitives.

In this example there are two different worlds \emph{server} and \emph{home}.
In the first line, we make valid the result of a piece of code executed on
the server. 
\emph{hold} is used to obtain a pointer to the result of $checksig \, sig$,
this is \emph{mobile} but we will need to be at the location \emph{server}
to access to find its original value.
The typing judgment for \emph{checked\_sig} is here
 $checked\_sig \sim string \, option \, at \, server $ .

In the second part, we are at the server location and
can find the original value of the result of $checksig\, sig$ using
\emph{leta}.

We then, according to this result, change the executing location to
home in order to display a string in the web browser used by the client.


\subsection{Security issues}

The problem of ML5 we now want to address is the lack of security,
one part of the code is executed on the client side, therefore
it cannot be trusted, however arbitrary continuations can be
passed from the client to the server, giving the client potential
access to any field in the database.
We address this issue by using the ideas of proof carrying authorization.


