%; 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:}\special{html:}}
\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:}#2\special
{html:}}
\def \softtarget #1#2{\special
{html:}#2\special
{html:}}
\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