%; tx     tx $*.tex
%; dview  dview -mlslides $*.dvi &
%; whizzy  slide -dvi "dview -mlslides."

\documentclass [landscape,semlayer,semcolor,semlcmss]{seminar}

\def \prsl {\green}
\usepackage {xprosper}
\def \jumpto #1{\special{html:<A href="jumpto:#1">}\special{html:</A>}}
\def \here #1{\hypertarget{#1}{}}

% \RequirePackage{semhelv}
% \ptsize{14}

%\input semlcmss.sty
%\usefont{T1}{phv}{m}{n}\fontsize{14.4pt}{12pt}\selectfont
%\usefont{T1}{phv}{m}{n}\fontsize{14.4pt}{14pt}\selectfont


\usepackage {amssymb}
\usepackage {pst-node}
\usepackage {hyperref}

%%% colors
\usepackage {color}
\definecolor{lightblue}{rgb}{0.7,0.7,1}
\definecolor{lightred}{rgb}{1,0.8,0.8}
\definecolor{lightgreen}{rgb}{0.6,1,0.6}


%%% both prosper and advi define the same macro pause, to be fixed

\let \Pause \pause
\let \pause \relax
\usepackage {advi}
\let \pause \Pause

\def \subpar #1{\par\medskip {\blue\bf #1}}
\let \partitle \subpar
\def \programcolor {\red\rm}
\def \jc {\@\triangleright\@}
\def \jcand {\@\&\@}

%\twoup
%\slidesmag{1}


%\slideframe {plain}\slideframewidth 0.1mm\slideframesep  4mm 
\slideframe {none}
%\renewcommand{\slideleftmargin}{-1cm}
\renewcommand{\slidetopmargin}{20pt}
\renewcommand{\slidebottommargin}{1cm}

\iftrue
\newpagestyle {mystyle}{}{}%{\hfil {\tiny \thepage}}
\pagestyle {mystyle}
\fi

\def \tf {\blue \bf}


%\pagestyle {plain}

\makeatletter 
\def \verbatim@font {\tt\red}
\makeatother


\iffalse
 \let \progfont  \rm
 \let \sltt \sl

 \let \progfont \tt
  \font \progfont  cmss10 scaled 2000
  \font \sltt  cmssi10 scaled 2000

 \def \progsize {\normalsize \progfont\baselineskip 0.0pt}
 \def \progstyle {\progsize \progfont }

 \def \progstyle {\progsize \progfont  \progcolor}
 \let \progcolor \black
 \def \reset {\progfont \progcolor}
 \def \reply {\sltt \red}
\fi

\let  ~ \hfill

\def \slidetitle #1{\begingroup 
   \sl \bf \purple {#1}\hfill {\tiny \thepage}\hbox{}\par
   \smallskip\hrule\medskip \endgroup} 
\def \titlestyle {\color{cyan}}

\renewcommand{\slidetitle}[1]{\vskip 2ex \subsection* 
{\centerline {\titlestyle \Large #1}}
}
\let \sameslide \newslide

\let \l \ell
\let \r \rho
\def \ebox #1{\colorbox{yellow}
   {\mbox {\large \strut #1}}}
\def \ie.{{\em i.e.}}
\let \@\;
\def \mathprefix #1{\mathopen{}\mathrel{\tt {#1}}}

\begin{document}

\pagestyle {empty}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pagestyle {mystyle}
\def \title #1{\paragraph* {\tf #1}}
\overlays*{\begin{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\slidetitle {General goal \vadjust {\vbox 
{\color{red}\hrule height 4pt}}}

\large
Design a language 
\begin {itemize}
\item
for concurrent and \ebox {\red \bf distributed} programming
\item that is both \ebox{\red \bf expressive} and
\ebox{\red \bf safe}

\item[]
(\ie. it should allows to reason about programs, 
including types, program analyses, proofs)
\end {itemize}

\end{slide}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\overlays*{\begin{slide}
\slidetitle{Specific goals in this work}

\large

A concurrent, object-oriented calculus with:
\vspace {0.5em}
\begin {itemize}
\item 
\ebox {\bf \red object internal concurrency}

%\fromPause[1]{
--- not just sequential objects running concurrently!
%}{}

\item
\ebox {\bf \red incremental assembling of object definitions}

%\pause[2]
 --- including the refinement of both
\begin {itemize}
\item behavior ~{\sl traditional in object-orientation}
\item synchronization ~{\sl expected in a concurrent setting}
\end {itemize}
\end {itemize}

\end{slide}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\overlays*{\begin{slide}
\slidetitle {Definition of behaviors in the $\pi$-calculus}
%\jumpto {after-pi}

\large
$$
\def \u{\mbox {\large \bf u\hskip 0.3ex}}
\def \z{\mbox {\large \bf z\hskip 0.3ex}}
\begin{array}{@{}ccccc}
&& 
\bulle %[=1]
    {\ovalnode* [fillstyle=solid,fillcolor=lightred]{u1}
        {\u?(x)\,P}}(0.2,-1.5){\mbox{Reception on $u$}} & 
\\
\hfil
\bulle %[=1]
  {\ovalnode* [fillstyle=solid,fillcolor=lightred]{u2}
        {\mathprefix {rec}{\u?(x) \, Q}}}
  (-1,-2)
  {\begin{minipage}{7em}Replicated \\reception on $u$\end{minipage}}&  
\\
& 
\bulle %[=1]
  {\ovalnode* [fillstyle=solid,fillcolor=lightgreen]{u3}
        {\hbox{$\u!(v)$}}}
   (2,-2)
   {\mbox{Emission on $u$}}
%\pause
& 
&& 
\fromPause[1]{\ovalnode* [fillstyle=solid,fillcolor=lightgreen]{u3b}
        {\hbox{$\u!(w)$}}}
\\[2ex]
\ifpause[=3]{\CancelColors}{}
\betweenPauses23
  {\ovalnode* [fillstyle=solid,fillcolor=lightblue]{u5}
        {\hbox{$dyn!(\psframebox*[fillstyle=solid,fillcolor=lightred]{\u})$}}
}
\RestoreColors
\hfill
\\
&
\betweenPauses23{\rnode{u45}{\color{blue}\star}}& 
\fromPause[3]{\ovalnode* [fillstyle=solid,fillcolor=lightred]{u6}{\u?(x) \, S}}
\\
\ifpause[=3]{\CancelColors}{}
\betweenPauses23{\ovalnode* [fillstyle=solid,fillcolor=lightblue]{u4}
  {dyn?(\psframebox*[fillstyle=solid,fillcolor=yellow]{\z}) 
        \psovalbox*[fillstyle=solid,fillcolor=lightred]
          {{\psframebox*[fillcolor=yellow]{\z}}{?(x) \,S}}}}
\hskip -3em
\RestoreColors
\\
\end{array}
\ncarc[linestyle=dashed,linecolor=red]{-}{u2}{u1}
\ncarc[linecolor=green]{-}{u3}{u1}
\ncarc[linecolor=green]{-}{u2}{u3}
\fromPause*[1]{
\ncarc[linecolor=green]{-}{u3b}{u1}
\ncarc[linecolor=green]{-}{u2}{u3b}
}
\betweenPauses*23{
\ncarc[linecolor=green]{-}{u45}{u4}
\ncarc[linecolor=green]{-}{u5}{u45}
}
\fromPause*[4]{
\ncarc[linecolor=green]{-}{u3}{u6}
\ncarc[linecolor=green]{-}{u3b}{u6}
\ncarc[linestyle=dashed,linecolor=red]{-}{u6}{u2}
\ncarc[linestyle=dashed,linecolor=red]{-}{u1}{u6}
}
\onlyPause*[3]{
\ncarc[linecolor=lightblue,doubleline=true]{<-}{u6}{u45}
}
$$
\vskip -6em
\null
\pause[4]

\large
\slidetitle{\leftline {\fromPause[2]{\ebox{Too loose!}}}}
\begin {itemize}
\pause
\item
{\ifpause[>0]{\color{gray}}{}
Behaviors attached to a name are not syntactically
known; they are reconfigurable, dynamically.}

\item
{\ifpause[>0]{\color{gray}}{}
This makes reasoning {\em and} distributed computing difficult.}
\pause
\end {itemize}

\end{slide}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\here {after-pi}
\overlays*{\begin{slide}
%\jumpto {after-join}
\slidetitle {Definitions of behavior in the join-calculus}

\large
$$
\def \u{{\mbox {\large \bf u\hskip 0.3ex}}}
\def \w{{\mbox {\large \bf w\hskip 0.3ex}}}
\def \jc {{}\@\triangleright\@{}}
\def \jcand {\@\&\@}
\hfill
\begin{array}{ccccc}
\bulle%[=1]
{\rnode {u0}{\psframebox* [fillstyle=solid,fillcolor=lightred]
{\begin{array}{r@{}l} \u(x) \jc& P\\ \u(x) \jcand \w(y) \jc &Q\\
\end{array}}}}
(-0.5,-3)
{\mbox{\begin{minipage}{9em}
 Defines synchronizing names $\u$ and $\w$ 
 and their behaviors altogether
\end{minipage}}}
&
\hspace {4em}
\begin{array}{cc}
\bulle%[=1]
{\ovalnode* [fillstyle=solid,fillcolor=lightgreen]{u1}{\u!(v)}}
(1,-2)
{\mbox{\begin{minipage}{6em}Asynchronous emission on $\u$\end{minipage}}}
\pause
\\
& 
\fromPause[1]{\ovalnode* [fillstyle=solid,fillcolor=lightgreen]{u2}
{\w!(v)}}
\\
\end{array}
\\
\betweenPauses23{\circlenode*{?}{\ldots}} \hfil
&\fromPause[3]
{\ovalnode* [fillstyle=solid,fillcolor=lightgreen]{u3}{\u!(k)}}\hfil
\\
\betweenPauses23{
\hfill \circlenode* {s}{\color{blue}\star}
}
\\[1em]
\ifpause[=3]{\CancelColors}{}
\betweenPauses23{
\rnode {xy}{\psframebox* [fillstyle=solid,fillcolor=lightblue]
      {dyn(\psframebox* [fillcolor=yellow]{z}) \jc
      {\psovalbox* [fillstyle=solid,fillcolor=lightgreen]
      {\psframebox* [fillcolor=yellow]{z}!(k)}}
}}
}
\RestoreColors
\hfill 
&
\\
\end{array}
\ncarc[linecolor=green]{u0}{u1}
\fromPause*[1]{\ncarc[linecolor=green]{u2}{u0}}
\betweenPauses*23{
\ncarc[linecolor=lightblue]{s}{xy}
\ncarc[linecolor=lightblue]{?}{s}
}
\onlyPause*[3]{
\ncarc[linecolor=lightblue,doubleline=true]{<-}{u3}{s}
}
\fromPause*[4]{
\ncarc[linecolor=green]{u3}{u0}
}
$$
\vskip -3em
\pause[4]
\null
\begin {itemize}
\pause \item
{\ifpause[>0]{\color{gray}}{}
Name scoping is more constrained than in $\pi$-calculus}

\onlyPause*{\em
\begin {itemize}
\item
Behavior of a name is statically defined and lexically scoped. 

\item
Synchronizing names are jointly defined.
\end {itemize}}

\pause \item
{\ifpause[>0]{\color{gray}}{}
Easier for reasoning and  distributed computation}
\end {itemize}

\pause
\vspace {1em}
\centerline {\ebox {\LARGE {But it's too rigid!}}}

\end{slide}}
\here {after-join}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}












































































%%%%%%%%%%%%%% macros %%%%%%%%%%%%%%%%%

\localmacros

\usepackage{array}
\usepackage{tabularx}
\let \Tabular \tabular \let \endTabular \endtabular
%\newenvironment{Tabular}[2][]{\begin{tabular}{#2}}{\end{tabular}}

\newcolumntype{S}{@{\extracolsep{\fill}}}
\newcolumntype{s}{@{\extracolsep{0em}}}
\newcolumntype{Z}{Scs}

\newcolumntype{C}{>{${}}c<{{}$}}
\newcolumntype{L}{>{${}}l<{{}$}}
\newcolumntype{R}{>{${}}r<{{}$}}
\newcolumntype{.}{@{}}
\newcolumntype{+}{>{\qquad}}
\newcolumntype{Y}[1]{>{\setlength{\hsize}{0.#1\hsize}}X}



%\def \require #1{\input {#1.def}}\def \provide #1{}

\scrollmode
\def \comment #1{\relax}

\makeatletter


%%% To change size in math mode

\let\Ts=\textstyle
\let\Ds=\displaystyle
\let\Ss=\scriptstyle

%%% Abrevs

\let \comp \circ
\let \wild \_


%%% To put text between two formulas on the same line

\def\text#1{\qquad\hbox{#1}\qquad}

%%%  Macros for mathematics

%% Special symbols

\def \nat {{\mathord{I\kern -.33em N}}}
\def \natb {{\mathord{I\kern -.33em\overline{N}}}}

\def\Vdash {\mathrel{\hbox{\vrule\kern .1ex$\vdash$}}}
\def\VVdash {\mathrel{\hbox{\vrule\kern .2ex\vrule\kern .1ex $\vdash$}}}

% An open box to end demonstrations with

\def\Box{\hbox
  {\vbox
    {\hrule height .033em
     \hbox to .5em
       {\vrule width .033em
        \hbox{\vbox to .5em{\vss}\hss}
        \vrule width .033em}
     \hrule height .033em
    }}}


%% Balanced symbols

\def\absolute#1{\mathopen\mid#1\mathclose\mid}

%% Operators

%\def \domain {\dv}
%\def \domain {\dvmathop{\sl dom}}
\def \domain #1{\mbox{\sl dom}(#1)}
\def \image {\mathop{\sl im\,}}
\def \codomain #1{\mbox{\sl cod}(#1)} %{\mathop{\sf cod\,}}

\def \modulo {\mathbin{\rm modulo}}
\def \inverse{{}^{-1}}
\def \cardinal {{\sl Card\,}}
%\def \restrict #1{\mathbin{\mid}_{#1}}
\def \restrict
   {\mathbin{\hbox{$|$\kern-.24em\lower.09em\hbox{\rm\char'22}$\!$}}}
\let \arity = \varrho


%% Quantifiers

\def \fall #1,{\forall #1,\;}
\def \exist #1,{\exists #1,\;}
\def \qt #1.{\forall\,#1.\,}
\def \ex #1.{\exists\,#1.\,}

%% Arrows

\let\ar=\rightarrow
\let\dar=\Rightarrow
\def\imply{\Longrightarrow}


\def \join {\mathrel {\&}}
\def \rewrite {\mathrel{-}\joinrel\leadsto}
\def \classrwarg #1{\stackrel{#1}{\leadsto}}
\def \classrw {\@ifnextchar [{\classrwarg}{\leadsto}} %]

%% Equalities

%\def \axiom {\mathrel {\mathop =^!}}
\def \axiom {=}
%\def \eqdef {\mathrel {\mathop {=\joinrel=}\limits^{def}}}

%% Sizes

\def\({\left(}
\def\){\right)}

\def\Mid{\mathrel{\Big|}}

%% Indices  see also indices.def

\def \ind #1#2{_{#1\in[1,#2]}}

%%

%% names 

\let \th \vdash
\let \tth \Vdash
\let \ttth \VVdash
\let \thh \models

\def\Cal#1{{\cal #1}}

\let \eset = \emptyset



%% Aligned constructions in math mode

% For internal use only

\def\noskip{\lineskiplimit=\the\lineskiplimit
                \lineskip=\the\lineskip}
\def\moreskip{\lineskiplimit=0.4em\lineskip=0.4em plus 0.2em}
\def\moremoreskip{\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}

\def\vatrix#1{\null\,\vcenter{\normalbaselines\moreskip\m@th
    \let \and \cr
    \ialign{$\displaystyle##$\hfil
      &\quad$\displaystyle##$\hfil&\quad##\hfil\crcr
      \mathstrut\crcr\noalign{\kern-\baselineskip}
      #1\crcr\mathstrut\crcr\noalign{\kern-\baselineskip}}}\,}

% A sequence of expressions is writen on separate lines to form one expression

\def \band #1{\left\{\vatrix{#1}\right.}          % brace and
\def \wand #1{\wedge\band{#1}}                    % wedge  and
\def \vand #1{\vee\band{#1}}                      % vee  and
\def \vor  #1{\vee\left[\vatrix{#1}\right.}       % vee and or
\def \Wand #1{\bigwedge\band{#1}}                 % big wedge and
\def \Vand #1{\bigvee\band{#1}}                   % big vee and
\def \Wor  #1{\bigvee\left[\vatrix{#1}\right.}    % big vee and



% A general usage tabulation in math mode.
%     Indentation is alternatively left and right, so that good place for
%     tabs will produce many different

% \dalign { & blabla :& blabla    \cr 
%           &    bla :& blablabla \cr
%         }
 
% \dalign {  blabla :&& blabla    \cr 
%            bla :   && blablabla \cr
%         }
 
% \dalign { & blabla :&    blabla \cr 
%           &    bla :& blablabla \cr
%         }

% Internal and personal use
\def\Dalign#1#2{\vcenter
 \bgroup
   \let\>=\qquad
   \def\title##1{\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}
%   \halign{$##$\hfil\qquad&&\hfil$##{}$&${}##$\hfil\qquad\cr#2\crcr}
%   \halign{$##$\hfil&&\qquad\hfil$##{}$&${}##$\hfil\cr#2\crcr}
   \halign{&${}##$\hfil&\hfil$##{}$\cr#2\crcr}
 \egroup}
% End internal use

\def\align#1{\vcenter
 \bgroup
   \let\>=\qquad
   \halign{#1\crcr}
 \egroup}

%\def\aligndef#1#2{\expandafter\def\csname aligndef#1\endcsname{#2}}
%\aligndef ]{\argalign}
%\aligndef l{&\hfil$##{}$}
%\aligndef r{&${}##$\hfil}
%\aligndef c{&\hfil$##$\hfil}
%\aligndef -{\qquad}
%\aligndef L{&\hfil##$}
%\aligndef R{&##\hfil}
%\aligndef C{&\hfil##\hfil}
%\def\argalign#1{\relax}
%\def\prealign#1{\csname aligndef#1\endcsname\prealign}
%\def\doalign#1]{\dohalign{\prealign#1]}}
%\def\dohalign#1#2{\expandafter\halign{#1\cr#2\crcr}}



%\def\dalign#1{\ifx#1[\doalign\else\Dalign3{#1}\fi}
\def\dalign{\Dalign3}


\def\Strut{\raise .4em\hbox{\strut}\raise -.4em\hbox{\strut}}

\def \deftitle #1
   {\def \title ##1
      {\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}}



\bgroup
 \catcode `\^^M \active
 \gdef \obeycr {\catcode `\^^M\active \let ^^M\crcr}
\egroup


\ifx \csname linewidth\endcsname \hsize 
 \let  \realwidth \hsize 
\else
 \let \realwidth \linewidth
\fi

\def \Mid {\mathrel{\Big\vert}}
\let \syntaxor \mid
\def \syntaxoris {\crcr \syntaxor&}
\def \syntaxtable #1
  {\def\is {::=&}\let \or \syntaxor \let \oris \syntaxoris
   \def \\{\cr\noalign{\medskip}}\def\cont{\cr&}\vbox 
   \bgroup
   \tabskip=100pt plus 1000pt minus 1000pt
   \halign to \realwidth
       {\hfil$##{}$\tabskip=0pt&
        ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
        &##\hfil \cr#1\crcr}
   \egroup}


\def \assertions #1
  {\deftitle2 \vbox
   \bgroup
     \halign {\hfil$##{}$&$##$\hfil&&\quad##\hfil\cr#1\crcr}
   \egroup}


%%% old version

\def\malign#1{\vcenter\bgroup
   \deftitle #1
   \def \lign ##1\cr {\noalign {##1}}
   \def \textlign##1{\noalign {\medskip \vbox {\noindent ##1}\medskip}}
   \tabskip=100pt plus 1000pt minus 1000pt
   \halign to \realwidth
       {\hfil$##{}$\tabskip=0pt&
        ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
        &##\hfil&$##$\hfil&  \cr#1\crcr\egroup}}

\newif \ifhsize \hsizefalse

\newskip \nullskip \nullskip 0pt
\newskip \fullskip \fullskip 100pt plus 1000pt minus 1000pt
\def \maligntrue {\tabskip \fullskip
                   \halign to \realwidth \bgroup}
\def \malignfalse {\halign \bgroup}
\def \malign {\vcenter \bgroup \ifhsize \expandafter \maligntrue \else \expandafter \malignfalse \fi}
\def \endmalign {\crcr \egroup \egroup}

\def \makeword #1#2#3{\expandafter
   \def \noexpand#3{#2 {#1\expandafter \let \expandafter \dummy\string #3}}}

%\let \vect \overrightarrow

\def \uad {\hskip 0.5em}


\def \whereis {\leftarrow}
\def \where #1{ \{ {\let \is \whereis #1} \} }
%\def \dowhere #1\is#2\is{[\ifx#2\empty #1\else #2/#1\fi]}
\def \dowhere #1\is#2\is{[\ifx#2\empty #1\else 
		\raisebox{.24ex}{$#2$}/\raisebox{-.28ex}{$#1$} \fi]}
\def \where #1{\let \is \relax\dowhere #1\is\empty\is}



\let \closeplus\relax
\let \Empty \relax
\let \is \relax
\def \plus #1{\PLUS #1\is\is\END}
\def \PLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1\plustoken#2)\else #1\fi}
\let \plustoken \mapsto

\let \diverge \uparrow

\def \set #1{\{#1\}}
\def \sem #1{\lbrack\!\lbrack#1\rbrack\!\rbrack}


\def\mathrm #1{\mathrel {\rm #1}}
\let \coerce \leq
\makeatother

\makeatletter


%% see infer.doc for a documentation

% Judgements

\let\th=\vdash

% naming

\expandafter \ifx \csname name\endcsname\relax
   \def\name#1{\hbox{\sc #1}}\else \relax \fi

\def \labname #1{{\rm(\name{#1})}}
\let \lab = \labname
\def \clab #1{\hbox {$\smash {\lab{#1}}$}}
\newskip \beforelabskip \beforelabskip = 0.5em
\def \eqlab {\eqno \lab}



\if \relax \csname keywordstyle\endcsname  \let \keywordstyle \tt \fi

%\def \keyword #1{{\hbox {\keywordstyle #1}}}
\def \keyword #1{{\keywordstyle #1}}
\def \mathtoken #1{\ifmmode
   \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi}
\def \mathpostfix #1{\mathrel{\keyword {#1}}\mathclose{}}
\def \mathprefix #1{\mathopen{}\mathrel{\keyword {#1}}}
\def \mathinfix #1{\mathrel{\keyword {#1}}}

\def\ignorefirst #1{}
\def \lwt #1{\expandafter \lowercase \expandafter \bgroup 
  \expandafter \ignorefirst \string #1\egroup}


\def \makeprefix #1#2{\expandafter\def \noexpand #1{\mathprefix  {#2}}}
\def \makepostfix #1#2{\expandafter\def \noexpand #1{\mathpostfix  {#2}}}
\def \maketoken #1#2{\expandafter\def \noexpand #1{\mathtoken {#2}}}
\def \makeinfix #1#2{\expandafter\def \noexpand #1{\mathinfix {#2}}}

\def \makein #1{\expandafter\def
  \noexpand #1##1in{\keyword {\lwt #1}\,\,##1\,\,\keyword {in}\,\,}}

\let \@ \;
\def \Let #1=#2in{\keyword {let}\@ {#1 = #2} \@\keyword {in}\@}
\def \fun (#1){\keyword {fun}\@ #1 \rightarrow}
\def \type #1=#2in{\keyword {type}\@ #1 = #2 \@\keyword {in}\@}

\makeatother

\let \cont \kappa
\let \t \tau
\let \l \ell
\let \s \sigma
\let \tv \alpha
%\let \vect \bar

\def \Gen {{\rm Gen}}

\def \tplus #1{\TPLUS #1\is\is\END}
\def \TPLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1:#2)\else #1\fi}

%%%%%%%%%%%%%%% light programs

\makeatletter
\def \progstyle {\tt}
\newskip \programindent 
\programindent 10cm
\ifnum \hsize < \programindent \programindent 1em\else \programindent 4em\fi
\def \program {\par \begingroup 
    \medskip \parindent \programindent \@tempswafalse
    \frenchspacing \@vobeyspaces \let \par \programpar 
    \let \- \program@break
    \parskip 0em %\offinterlineskip
     \obeylines \progstyle 
    \catcode``=13 \@noligs \let \do \@makeother \dospecials 
    \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
    \prog@specials \prog@initspecials \obeyspaces }

\def \programpar {\if@tempswa\hbox{}\fi\@tempswatrue\@@par}

\bgroup
\gdef \less@specials {\relax
 \catcode `| \active 
 \catcode `< \active
 \catcode `> \active
 \catcode `- \active
 \catcode `_ \active
 \catcode `\' \active 
}
\gdef \more@specials {\relax
 \catcode `( \active
 \catcode `) \active
}
\gdef \prog@specials {\less@specials\more@specials}
\prog@specials
\gdef \prog@initspecials {\def
    -{\minus@program}\def
    _{\underscore@program}\def
    '{\acurate@program}\def
    |{\bar@program}\def
    <{\less@program}\def
    >{\greater@program}\def
    ({\leftparen@program}\def
    ){\rightparen@program}}
 \gdef \bar@@program {\let\do \eattoken
  \ifx \token >$\droite$\else ${}\mid{}$\let \do \relax\fi \do}
 \gdef \minus@@program {\let\do \eattoken
  \ifx \token >$\ar$\else -\let \do \relax\fi \do}
\egroup
\let \leftparen@program \less@program
\let \rightparen@program \greater@program
\def \underscore@program {\_}

\def \acurate@program {\futurelet \token \acurate@@program}
\def \acurate@@program {\let \do \eattoken
  \ifx \token a$\alpha$\else 
   \ifx \token b$\beta$\else 
    \char `\' \let \do \relax\fi\fi \do}
\def \less@program {\hbox{$<$}}
\def \greater@program {\hbox{$>$}}
\def \bar@program {\futurelet \token \bar@@program}
\def \minus@program {\futurelet \token \minus@@program}

\newskip \program@tmp


\def \programbreak #1#2{\program@tmp #2\hfil
   \penalty #1\hfilneg \nobreak \hskip -\program@tmp \hbox {}\nobreak
   \hskip \program@tmp}
\def \program@break {\programbreak {100}{3em}}

\def \endprogram {\ifdim\lastskip >\z@ \@tempskipa\lastskip 
       \vskip -\lastskip\fi\medskip \endgroup
     \@endpetrue}

\def\prog {\begingroup \hbox \bgroup
  \catcode ``=13 \@noligs
  \let \do \@makeother \dospecials \progstyle
   \prog@specials \prog@initspecials
    \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
  \@prog}
\def\@prog#1{\obeyspaces \frenchspacing \catcode `\  10
            \def\@tempa ##1#1{##1\egroup\endgroup}\@tempa}
\makeatother

%%%%%%%%%%%%%%%%%%%  "quotations"

\makeatletter
% on  active  le cararectere " et on s'en sert pour le mode \prog
% s'il est défini ou \verb autrement

\bgroup
\@makeother \"
\gdef \progquote {\prog"}
\catcode `\" \active
\gdef "{\progquote}
\egroup

\def \quoteon {
\let \quote@sanitize \@sanitize
\def \@sanitize {\quote@sanitize \@makeother\"}
\let \quote@specials \dospecials 
\def \dospecials {\quote@specials \do\"}
\def \quoteon {\catcode `\" \active}\quoteon}

\def \quoteoff {\@makeother \"}
\makeatother



%%%%%%%%%%%%%%%%
\def \lift #1{\;{}^{#1}}
\def \inu #1{\lift {i \in 1..#1}}
\def \jnu #1{\lift {j \in 1..#1}}

%% typo

\mathchardef \le "313C
\mathchardef \ge "313E

\mathcode `< "4268
\mathcode `> "5269

\def \makebaractive {\catcode `\| \active}
\everydisplay {\makebaractive}
\everymath {\makebaractive}
\bgroup
  \makebaractive
  \gdef |{\baractive}
\egroup

\let \olspecials \dospecials \def \dospecials {\olspecials \do \|}

\def \droite {\mathrel {\,\hbox {\large$\triangleright$}\,}}

\makeatletter
\def \baractive {\futurelet\token \next@baractive}
\def \eattoken #1{}
\let \Pjoin \mid
\def \next@baractive{\let\do\eattoken
    \ifx \token>\ifmmode \droite\else $\droite$\fi
         \else \ifmmode \mid \else $\Pjoin$\fi
         \let \do \relax \fi \do}


\def \Def #1in{\mathprefix {{\sf def}}#1\mathinfix{{\sf in}}}
\def \Let#1in{\mathprefix {let}#1\mathinfix{in}}
\def \Reply#1to{\mathprefix {reply}#1\mathinfix{to}}
%\def \>{\droite}
\def \And {\mathrel{\wedge}}
\def \tuple #1{\langle#1\rangle}
\def \v {\varphi}


\let \bcup \cup
\let \thd \th
\def \defines {::}
\def \produces #1{\Ds\mathop{\Longrightarrow}^{#1}}
\def \RED {\longrightarrow}
\let \redcham \mapsto

\let \plus \tplus

\makeatother
 

\def \dd {{\cal D}}
\def \pp {{\cal P}}

\def \dv #1{\mbox{\sl dl}(#1)}

\def \redsoupe {\mathrel {\mathop {\red} \limits^s}}
\let \redstruct \rightleftharpoons
\let \redchaud \rightharpoonup
\let \redfroid \leftharpoondown
\let \cool \leftharpoondown
\let \heat \rightharpoonup

\def\redstep{\mathrel{\mathpalette\redstepaux{}}}
\def\redstepaux#1{\vcenter{\hbox{\ooalign{\hfil
      \raise2pt \hbox{$\rightharpoonup$}\hfil\cr\hfil
      \lower2pt\hbox {$\leftharpoondown$}\hfil\crcr
      $\longrightarrow$}}}}


\def \Comment #1{}
\let \agree \approx
\quoteon

\maketoken \int {int}


\def \Obj#1in{\mathprefix{{\sf obj}}#1\mathinfix{{\sf in}}}

%\def \Class#1in{\mathprefix{{\sf class}}#1\mathinfix{{\sf in}}}
%\def \New#1in{\mathprefix{{\sf new}}#1\mathinfix{{\sf in}}}


\def \dowhere #1\is#2\is{\{\ifx#2\empty #1\else \subst {#2}{#1}\fi\}}
\def \/{\hskip 0em\hbox {$\,\wedge\,$}}
\def \/{\infix {or}}

\makeatletter
\let \leftparen@program (
\let \rightparen@program )
\makeatother

\def \vs.{{\em vs.}}
\def \resp.{respectively}
\def \eg.{{\em e.g.}}
\makeprefix \obj {obj}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% the objective join-calculus : macros
% ===========================================

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

% the proof environment

\newenvironment{proof}{\begin{trivlist}
\item[\hspace{\labelsep}{\em\noindent Proof: }]
}{\qed\end{trivlist}}

%definition of qed |__|
\def \whitebox{{\hbox{\hskip 1pt
        \vrule height 6pt depth 1.5pt
        \lower 1.5pt\vbox to 7.5pt{\hrule width
                  3.2pt\vfill\hrule width 3.2pt}%
        \vrule height 6pt depth 1.5pt
        \hskip 1pt } }}

\def \qed{\ifhmode\allowbreak\else\nobreak\fi\hfill\quad\nobreak
    \whitebox\medbreak}

% end of the proof environment





% parts temporarily removed from the conference paper

\makeatletter
\def\commentpar#1{%
  {\def\@latex@warning@no@line##1{}\marginpar{#1}}}
\makeatother
\def\namedcomment#1#2{\commentpar{\raggedright\footnotesize{\bf #1} #2}}
%\def\namedcomment#1#2{{\bf #1}: {\em #2}}
\let \Namedcomment \namedcomment
\addtolength{\marginparwidth}{10ex}
%\def\namedcomment#1#2{}


\if \relax \csname keywordstyle\endcsname  \let \keywordstyle \tt \fi

\def \keyword #1{{\keywordstyle #1}}
\def \mathtoken #1{\ifmmode
   \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi}
\def \mathpostfix #1{\mathrel{\keyword {#1}\mathclose{}}}
\def \mathprefix #1{\mathopen{}\mathrel{\keyword {#1}}}
\def \mathinfix #1{\mathrel{\keyword {#1}}}

\let \kwd \sf



\def \some #1{\nu (#1)}
\def \Some {\hbox {$\nu$}}
\def \mid {\; | \;}
\def \DEF {\mathprefix {\kwd def}}
\def \OBJ {\mathprefix {\kwd obj}}
\def \CLS {\mathprefix {\kwd class}}
\def \XDEF #1{\mathprefix {\kwd def}_{#1}}
\def \INDEF {\mathinfix {\kwd in}}
\def \NEW {\mathprefix {\kwd new}}
\def \nil {{\sf 0}}
\def \jsend #1#2{#1 \langle #2 \rangle}
\def \jeq {\mathop{\triangleright}}
\def \jrule #1#2{#1 \jeq #2}
\def \jand {\mathrel{\wedge}}

\def \kindofvar #1#2{{\sf #1}[#2]}
%\def \dv #1{\kindofvar{dv}{#1}}
\def \fv #1{\kindofvar{fv}{#1}}
\def \xv #1{\kindofvar{xv}{#1}}
\def \ov #1{\kindofvar{ov}{#1}}
\def \cv #1{\kindofvar{cv}{#1}}
\def \rv #1{\kindofvar{rv}{#1}}
\def \iv #1{\kindofvar{iv}{#1}}
\def \fw #1{\mbox{\sl vw}(#1)}

\def \Vdash {\mathrel{\hbox{\vrule\kern .1ex$\vdash$}}}
\def \names{{\cal V}}
\def \is {::=}
\def \th {\vdash}
\def \plus {+}
\def \l {\ell}
\def \Ocaml {{\sc objective caml}}
\def \inherit {\; {\sf inherit} \; }
\def \init {\; {\sf init} \; }
\def \self {{\sf self}}
\def \this {{\sf this}}
\def \public #1#2{\; {\sf public} \; #1 \; {\sf of} \; #2}
\def \ovrr #1{\; {\sf overriding} \; #1}
\def \>> {$\rangle$}
\def \<< {$\langle$}
\def \hole {\cdot}

\newcommand{\cosimo}[1]{\namedcomment{Cosimo}{#1}}
\newcommand{\cedric}[1]{\namedcomment{Cedric}{#1}}
\newcommand{\didier}[1]{\namedcomment{Didier}{#1}}
\newcommand{\luc}[1]{\namedcomment{Luc}{#1}}

\newcommand{\Cosimo}[1]{\Namedcomment{Cosimo}{#1}}
\newcommand{\Cedric}[1]{\Namedcomment{Cedric}{#1}}
\newcommand{\Didier}[1]{\Namedcomment{Didier}{#1}}
\newcommand{\Luc}[1]{\Namedcomment{Luc}{#1}}

\newcommand{\tuplet}[1]{( #1 )} % Type of messages
\newcommand{\tuplea}[1]{\langle #1 \rangle}
\newcommand{\RCHAM}{\mbox{\sc rcham}}
\newcommand{\rulename}[1]{\mbox{\sc (#1)}}
\newcommand{\rulenamesmall}[1]{\mbox{\small {\sc (#1)}}}
\newcommand{\defin}[2]{\DEF #1 \INDEF #2}
\newcommand{\object}[2]{\OBJ #1 \INDEF #2}
\newcommand{\class}[2]{\CLS #1 \INDEF #2}
\def \class #1=#2in{\prefix {class} #1=#2 \infix{in}}
\def \obj #1=#2in{\prefix {obj} #1=#2 \infix{in}}

\newcommand{\new}[2]{\NEW #1 \INDEF #2}
\newcommand {\subst} [2] {\raisebox{.24ex}{$#1$} / \raisebox{-.28ex}{$#2$}}
\newcommand{\eqdefshort}{\mathrel{\stackrel{\rm\mbox{\tiny def}}{=}}}
\newcommand{\eqdef}{\;\eqdefshort\;}
\newcommand{\vect}[1]{\widetilde{#1 } }
\newcommand{\bigfract}[2]{\frac{^{\textstyle #1}}{_{\textstyle #2}}}
\newcommand{\subs}[4]{#1 [ \raisebox{.24ex}{$#2$} /
                      \raisebox{-.28ex}{$#3$} , \, #4 ]}
\newcommand{\super}[1]{{ }^{#1}}



\def\redstepaux#1{\vcenter{\hbox{\ooalign{\hfil
      \raise2pt \hbox{$\rightharpoonup$}\hfil\cr\hfil
      \lower2pt\hbox {$\leftharpoondown$}\hfil\crcr
      $\longrightarrow$}}}}
\def\redstep{\mathrel{\mathpalette\redstepaux{}}}

\def \barb#1{\mathpostfix{\Downarrow_{\it #1}}}

\def \athrule #1#2#3{\begin{array}{l} {\scriptstyle (\hbox{\sc #1})} 
\\ \bigfract{#2}{#3}
\end{array}}

\def \mathax #1#2{\begin{array}{l} {\scriptscriptstyle \hbox{\sc #1}} \\ #2
\end{array}}


\let \cool \leftharpoondown
\let \heat \rightharpoonup
\let \heatcool \rightleftharpoons
\let \reduce \longrightarrow

%\let \obj \object

\def \names {\cal U}
\def \methodnames {\cal M}
\def \privatenames {\cal L}
\def \AND {\mathpostfix {}\mathop {\mathtoken {and}}\limits}

\def \bframe #1{\fbox \bgroup \vbox \bgroup}
\def \eframe{\egroup \egroup}
\newenvironment {framed}
    {\fboxsep 0.6em
     \advance \hsize by -2\fboxsep
     \advance \hsize by -2\fboxrule
     \setbox0 \vbox \bgroup}
    {\egroup \noindent \fbox {\box0}}

\def \hidecomment #1{} 
\def \private #1{\uppercase {#1}}
\let \Public \overline

\def \Class #1in{\CLS #1\INDEF}
%\def \New #1in{\NEW #1\INDEF}
\makeprefix \New {\mbox{\sf new}}
\def \Gen {\mathop {\hbox {\sl Gen}}}
\makeinfix \Realloc {realloc}
\makeinfix \Alloc {alloc}


\def \ge {$>$}
\def \eqdef {\mathrel {\mathop=\limits^{\triangle}}}

\let \leadsto \rightsquigarrow


\makeprefix \inherit {inherit}
\def \vect #1{\widetilde {#1}}
\def \objectnames {{\cal O}}
\def \classnames {{\cal C}}
\def \labels {{\cal L}}
\def \views {{\cal V}}
\makeinfix \Hide {hide}
\makeinfix \as {as}
\let \+ \oplus


\let \r \rho
\let \rv \varphi
\def \sig #1{\hbox {$\varsigma($}#1\hbox{$)$}}
\def \sig #1{\mathprefix {self(#1)}}

\def \Sig #1{\hbox {$\zeta(#1)$}}
\let \st \chi
\def \objtype #1{[#1]}

\def \meth {{\cal M}}
\def \var {{\cal U}}
\def \alias {{\cal S}}

\let \mell m
\let \fell l
\let \sell s

\def\syntaxdef{\mathrel{::=}}
\def\syntaxpar{\;\;\mathrel{\ \rule[-1ex]{0.4pt}{3ex}\ }\;\;}

\newcommand{\mysyntax}[1]{
  \def\entry##1[##2]##3[##4]{
    {##1} & \syntaxdef & \hspace{4cm} & \!\!\!\! \mbox{##2}
    \\    &            & {##3} & \mbox{##4} }
  \def\oris##1[##2]{ 
    \\    & |   & {##1} & \mbox{##2} } 
  \def\orisopt##1[##2]{ 
    \\ \left(   & |   & {##1} & \mbox{##2} \right) } 
  \begin{array}{rcll}
  #1
  \end{array}
  }


%%% for twocolumn
\renewcommand{\mysyntax}[1]{
  \def\entry##1[##2]##3[##4]{
    {##1} & \syntaxdef & & \mbox{\bf ##2}
    \cr    &            & {##3} & \mbox{##4} }
  \def\oris##1[##2]{ 
    \cr    & |   & {##1} & \mbox{##2} } 
  \def\orisopt##1[##2]{ 
    \cr \left(   & |   & {##1} & \mbox{##2} \right) }
  \def \\{\cr\noalign{\vskip 2ex}}
  \vbox {\tabskip 0em plus 1fil
  \halign to \hsize{$##$\hfil\tabskip = 0em
         &\hfil${}##{}$\hfil&$##$\hfil\tabskip =0em plus 1fil 
         &\quad $##$\hfil\cr #1\crcr}}
  }

% CF: report macros when Didier is back
% beware, \rv stands for raw variable, not for received variables (\bv)

\def \kindofvar #1#2{{\sf #1}(#2)}
\def \bv #1{\kindofvar{rv}{#1}}
\def \kindoflabel #1{#1}
\def \sell {\kindoflabel{s}}
\def \fell {\kindoflabel{f}}
\def \mell {\kindoflabel{m}} 
\def\plan#1.{\namedcomment{}{\em#1}}
\def \opublic {opublic}

\font\twentysltt=cmsltt10 scaled 2400
\font\elevensltt=cmsltt10 scaled 1100
\font\tensltt=cmsltt10
\font\ninesltt=cmsltt10 scaled 900
\font\eightsltt=cmsltt10 scaled 800


\makeprefix \view {view}
\def \doforward #1\is#2\is{[\ifx#2\empty #1\else #1 \mapsto #2\fi]}
\def \forward #1{{\let \dowhere \doforward\where {#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% New (cleaner) macros 

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage {mathpartir}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage {listings}
\lstset{style=RGB,escapechar=\%,indent=0em,%
%  flexiblecolumns=false,%
  outputpos=r,%
  identifierstyle=\textcolor{black},%
  }
\let \lst \lstinline

\let \e \epsilon

\let \D \Phi
\let \D \Gamma
\def \V {\Theta}
\let \eset  \emptyset
\let \Dv \theta
\def \objtype #1{[#1]}

%\let \T \Delta
%\let \Tv \delta
\let \rv \varrho
\def \A {\bar A}
\let \A \Gamma
\def \none {{\star}}
\def \splus {\mathbin{/}}
\makeatother

\def \return{reply}
\def \ITEM{\\\hbox {\ \ --}}

\def \[#1]{{\bracketcolor #1}}
\let \bracketcolor \blue

\usepackage {hevea}
%%%%% emphasize 
\ifhevea 
\def \colorbox #1#2{\begin{Tabular}
      [cellspacing=0 bgcolor=#1 border=0]{p{}}#2\end{Tabular}}
\newcommand{\psframebox}[2][]{\colorbox {yellow}{#2}}
\fi
\let \estrut \strut
%\psframebox [linecolor=yellow,fillstyle=solid,fillcolor=yellow]
\ifhevea
\def \evbox #1{\colorbox {yellow}{\large \estrut #1}}
\else
\def \evbox #1{\colorbox {yellow}
   {\hsize \linewidth \advance \hsize by -2\fboxsep 
    \advance \hsize by -2\fboxrule
    \vbox {\large \estrut #1}}}
\fi
\def \esbox #1{\colorbox{yellow}
   {\mbox {#1}}}
\def \embox #1{\ebox {$#1$}}
\newcommand \cmbox[3][]{\ifx #1\empty
%  \psframebox [linecolor=#2,fillstyle=solid,fillcolor=#2]
   \colorbox {#2}
      {\mbox {\large \estrut $#3$}}%
   \else 
%   \psframebox [linecolor=#2,fillstyle=solid,fillcolor=#2]
   \colorbox {#2}
      {\mbox {$#3$}}%
   \fi}

\let \hide \white

\newenvironment{file}[2][lightgreen]
    {\bgroup
     \abovedisplayskip 0.5\abovedisplayskip
     \belowdisplayskip 0.5\belowdisplayskip
     $$\vbox \bgroup 
     \def \file@color{#1}\def \@test{#2}\ifx \@test\empty %\@miniskip
     \else \centerline {\ttfamily\itshape #2}\fi
     \setbox0\vbox \bgroup \advance \hsize by -6.4pt\advance
       \linewidth by -6.4pt}
    {\egroup
%     \psframebox [linewidth=0.2pt,fillcolor=\file@color,fillstyle=solid]
     \noindent
     \fboxrule 0.2pt
     \colorbox{\file@color}{\box0}%\@miniskip
% \fbox{\box0}
     \egroup $$\egroup\ignorespacesafterend}


\let \eset \emptyset
\def \keywordstyle #1{{\sf #1}}
\def \keyword #1{\keywordstyle {#1}}
\def \token #1{\ifmmode
   \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi}
\def \postfix #1{\mathrel{\keyword {#1}}\mathclose{}}
\def \prefix #1{\mathopen{}\mathrel{\keyword {#1}}}
\def \infix #1{\mathrel{\keyword {#1}}}
\def \patch #1#2{\prefix {patch} #1\infix{with} #2\postfix {end}}
\let \rewrites \Rightarrow
\let \l \ell
\def \cl #1{\mbox{\sl cl}(#1)}
\let \th \vdash
\let \r \rho
\let \V \vect
\def \sig #1{\zeta(#1)}
\let \GM W
\let \GV X
\def \stack #1{{\let \\\crcr\vbox {\halign \bgroup $##$\hfil\cr #1\crcr\egroup}}}
\def \private {{\cal F}}
\def \public {{\cal M}}
\def \self #1{\token{self}(#1)\,}

\makeatletter
\edef\hyper@quote{\string"}
\edef\hyper@sharp{\string#}
\def \softlink #1#2{\special 
  {html:<A href=\hyper@quote\hyper@sharp#1\hyper@quote>}#2\special
  {html:</A>}}
\def \softtarget #1#2{\special
  {html:<A name=\hyper@quote#1\hyper@quote>}#2\special
  {html:</A>}}


\endinput


% LocalWords:  PE PS num Op fullstyle fv fil arg val pre abs int obj REF incr
% LocalWords:  EXT ext Ojoin init NB ajdunction dyn linestyle linecolor ccccc
% LocalWords:  lightblue fillstyle fillcolor lightred cc lightgreen xy lcr lr
% LocalWords:  rl dom def Ocaml escapechar Matsuoka Yonezawa typechecking
% LocalWords:  Odersky's JoCaml Ocaml's toplevel polymorphism sbuffer