\documentclass{seminar}
\usepackage{color}
\usepackage{graphics}
\usepackage{prooftree2}
\usepackage{pifont}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{myslides}

\sloppy

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

% IMPORTANT!

% To typeset this paper for color, use the first definition below.
% To typeset this paper for black and white, use the second definition.

\newcommand{\incolor}[1]{#1}    % Use to typeset in color
%\newcommand{\incolor}[1]{}     % Use to typeset in black and white

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

% color framework

\newcommand{\judgecolor}{}
\newcommand{\typecolor}{}
\newcommand{\termcolor}{}
\newcommand{\Typecolor}{}
\newcommand{\Termcolor}{}

\newcommand{\uncolored}{
  \incolor{
    \renewcommand{\judgecolor}{}
    \renewcommand{\typecolor}{}
    \renewcommand{\termcolor}{}
    \renewcommand{\Typecolor}{}
    \renewcommand{\Termcolor}{}
  }
}

\newcommand{\colored}{
  \incolor{
    \renewcommand{\judgecolor}{\color{black}}
    \renewcommand{\typecolor}{\color{blue}}
    \renewcommand{\termcolor}{\color{red}}
    \renewcommand{\Typecolor}{\color{cyan}}
    \renewcommand{\Termcolor}{\color{magenta}}
  }
}

\newcommand{\jd}[1]{{\judgecolor #1}}
\newcommand{\tp}[1]{{\typecolor #1}}
\newcommand{\tm}[1]{{\termcolor #1}}
\newcommand{\Tp}[1]{{\Typecolor #1}}
\newcommand{\Tm}[1]{{\Termcolor #1}}

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

% sequent calculus vs dual calculus framework

\newcommand{\seqdual}{\pickright}

\newcommand{\makesequent}{\renewcommand{\seqdual}{\pickleft}}
\newcommand{\makedual}{\renewcommand{\seqdual}{\pickright}}

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

% duality framework

\newcommand{\pickleft}[2]{#1}
\newcommand{\pickright}[2]{#2}

\newcommand{\makepickleft}{\renewcommand{\pick}{\pickleft}}
\newcommand{\makepickright}{\renewcommand{\pick}{\pickright}}

\newcommand{\pick}{\pickleft}
\newcommand{\swap}{\pick{\makepickright}{\makepickleft}}
\newcommand{\dual}[1]{\swap#1\swap}

\newcommand{\reorder}[2]{\pick{#1 #2}{#2 #1}}
\newcommand{\twice}[1]{#1\dual{#1}}

\newcommand{\twicedualseq}[1]{#1 \makesequent #1 \makedual}

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

% figures style

\setcounter{dbltopnumber}{1}
\setcounter{topnumber}{1}

\renewcommand{\dbltopfraction}{.85}
\renewcommand{\dblfloatpagefraction}{.85}
\renewcommand{\textfraction}{.15}

% figures

\newcommand{\figrule}{\rule{\columnwidth}{0.25ex}}
\newcommand{\Figrule}{\rule{\textwidth}{0.25ex}}
\newenvironment{fig}{\figrule}{\figrule}
\newenvironment{Fig}{\Figrule}{\Figrule}

\newcommand{\figcaption}[1]{\vspace{-4ex}\caption{#1}\vspace{2ex}}

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

% comment out

\newcommand{\eat}[1]{}

% propositions and notes

%\newcommand{\proposition}[1]{\textbf{Proposition}~~\emph{#1}}

\newtheorem{proposition}{Proposition}%[section]
%\newenvironment{note}{\begin{trivlist} \item \textbf{Note. }}{\end{trivlist}}

% useful environments

\newcommand{\synskip}{2ex}
\newcommand{\redskip}{2ex}
\newcommand{\transkip}{2ex}
\newcommand{\where}{\\[1ex]\mbox{where}\\[1ex]}

\newenvironment{rules}{\[\colored\ba{c}}{\ea\]}
\newenvironment{syntax}{\[\colored\ba{l@{\quad}lcl}}{\ea\]}
%\newenvironment{doublesyntax}{\[\colored\ba{l@{\quad}lcl{\quad}lcl}}{\ea\]}
\newenvironment{reductions}{\[\colored\ba{l@{\quad\quad}lcll}}{\ea\]}
\newenvironment{translation}{\[\colored\ba{lcl}}{\ea\]}

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

% arrays

\newcommand{\ba}{\begin{array}}
\newcommand{\ea}{\end{array}}

\newcommand{\triple}[3]{
 \[\colored
   \ba{lcl} \pick{#1}{#2} \ea \quad\quad \ba{lcl} \pick{#2}{#1} \ea
 \]
 \[\colored
   \ba{lcl} #3 \ea
 \]
}

\newcommand{\quadruple}[4]{
 \[\colored\makebox[0em]{$
  \ba{c}
   \ba{lcl} #1 \ea
   \\ \\
   \ba{lcl} \pick{#2}{#3} \ea \quad\quad \ba{lcl} \pick{#3}{#2} \ea
   \\ \\
   \ba{lcl} #4 \ea
  \ea
 $}\]
}

\newcommand{\quintuple}[5]{%
 \[\colored\makebox[0em]{$
  \ba{c}
   \ba{lcl} #1 \ea \quad\quad \ba{lcl} #2 \ea
   \\ \\
   \ba{lcl} \pick{#3}{#4} \ea \quad\quad \ba{lcl} \pick{#4}{#3} \ea
   \\ \\
   \ba{lcl} #5 \ea
  \ea
 $}\]
}

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

% type operators

\newcommand{\Top}{\pick{\top}{\bot}}
\newcommand{\Bot}{\dual{\Top}}
\renewcommand{\And}{\pick{\mathbin{\&}}{\mathbin{\vee}}}
\newcommand{\Or}{\dual{\And}}
\newcommand{\Not}{\neg}
\newcommand{\Implies}{\pick{\mathbin{\supset}}{\error}}

\newcommand{\Plus}{\mathbin{\Tp{+}}}
\newcommand{\Times}{\mathbin{\Tp{\times}}}
\newcommand{\Arrow}{\mathbin{\Tp{\pmb{\rightarrow}}}}

\newcommand{\error}{\typeout{************** ERROR ***************}*** ERROR ***}

% equivalence and reduction

\newcommand{\vn}{{\pick{v}{n}}}
\newcommand{\VN}{{\pick{V}{N}}}

\newcommand{\defeq}{\mathbin{\jd{\equiv}}}
\newcommand{\defeqtype}{\mathbin{\jd{\equiv}}}
\newcommand{\Defeq}{\mathbin{\jd{\equiv}}}
\newcommand{\Defeqtype}{\mathbin{\jd{\equiv}}}

\newcommand{\becomes}{\mathbin{\longrightarrow}}
\newcommand{\Becomes}{\mathbin{\longrightarrow}}

\newcommand{\becomesv}{\mathbin{\becomes_\vn}}
\newcommand{\becomesn}{\dual{\becomesv}}

% rule names

\newcommand{\Left}{\mathrm{\pick{L}{R}}}
\newcommand{\Right}{\dual{\Left}}

\newcommand{\Intro}{\mathrm{I}}
\newcommand{\Elim}{\mathrm{E}}

\newcommand{\Id}{\mbox{Id}}
\newcommand{\Thinning}{\mbox{Thinning}}
\newcommand{\Contraction}{\mbox{Contraction}}
\newcommand{\Interchange}{\mbox{Interchange}}
\newcommand{\Cut}{\mbox{Cut}}

% substitution and contexts

\newcommand{\fillhole}[1]{\{#1\}}
\newcommand{\hole}{\fillhole{\,}}
\newcommand{\sub}[3]{#1\fillhole{#2/#3}}

% free variables

\newcommand{\free}[1]{\mbox{free$(#1)$}}

% term operators - dual calculus

\newcommand{\pair}[2]{\pick{\langle#1,#2\rangle}{[#1,#2]}}
\newcommand{\case}[2]{\dual{\pair{\dual{#1}}{\dual{#2}}}}
\newcommand{\fst}[1]{\pick{\mbox{fst}[#1]}{\langle#1\rangle\mbox{inl}}}
\newcommand{\inl}[1]{\dual{\fst{\dual{#1}}}}
\newcommand{\snd}[1]{\pick{\mbox{snd}[#1]}{\langle#1\rangle\mbox{inr}}}
\newcommand{\inr}[1]{\dual{\snd{\dual{#1}}}}
\newcommand{\comp}[1]{\pick{[#1]\mbox{not}}{\mbox{not}\langle#1\rangle}}
\newcommand{\cocomp}[1]{\dual{\comp{\dual{#1}}}}
\newcommand{\bind}[2]{\pick{#1.(#2)}{(#2).#1}}
\newcommand{\cobind}[2]{\dual{\bind{\dual{#2}}{\dual{#1}}}}
\newcommand{\cut}[2]{\pick{#1 \mathbin{\bullet} #2}{#2 \mathbin{\bullet} #1}}

\newcommand{\dualabs}[2]{\pick{\abs{#1}#2}{*** ERROR ***}}
\newcommand{\dualapp}[2]{\pick{#1 \mathbin{@} #2}{*** ERROR ***}}

% continuation terms

\newcommand{\abs}[1]{\lambda#1.\,}
\newcommand{\aabs}[1]{\boldsymbol{\lambda}#1.\,}
\newcommand{\app}[1]{\,#1}
\newcommand{\apppar}[1]{\,(#1)}
\newcommand{\tpair}[2]{\langle #1,#2 \rangle}
\newcommand{\tinl}[1]{\mbox{inl}\,#1}
\newcommand{\tinr}[1]{\mbox{inr}\,#1}
\newcommand{\sumcase}[5]
  {\mbox{case\;$#1$\;of\;$\tinl{#2} \Rightarrow #3$,
                         $\tinr{#4} \Rightarrow #5$}}
\newcommand{\fstcase}[3]
  {\mbox{case\;$#1$\;of\;$\tpair{#2}{-} \Rightarrow #3$}}
\newcommand{\sndcase}[3]
  {\mbox{case\;$#1$\;of\;$\tpair{-}{#2} \Rightarrow #3$}}

\newcommand{\tfst}[1]{\mbox{fst}\,#1}
\newcommand{\tsnd}[1]{\mbox{snd}\,#1}
\newcommand{\tlet}[3]{\mbox{let $#1$ = $#2$ in $#3$}}

% variables

\newcommand{\expa}{\pick{M}{K}}
\newcommand{\expb}{\pick{N}{L}}
\newcommand{\expc}{\pick{M}{K}}
\newcommand{\coexpa}{\dual{\expa}}
\newcommand{\coexpb}{\dual{\expb}}
\newcommand{\coexpc}{\dual{\expc}}

\newcommand{\vala}{\pick{V}{P}}
\newcommand{\valb}{\pick{W}{Q}}
\newcommand{\valc}{\pick{V}{P}}
\newcommand{\covala}{\dual{\vala}}
\newcommand{\covalb}{\dual{\valb}}
\newcommand{\covalc}{\dual{\valc}}

\newcommand{\vara}{\pick{x}{\alpha}}
\newcommand{\varb}{\pick{y}{\beta}}
\newcommand{\varc}{\pick{z}{\gamma}}
\newcommand{\covara}{\dual{\vara}}
\newcommand{\covarb}{\dual{\varb}}
\newcommand{\covarc}{\dual{\varc}}

\newcommand{\expctx}{\pick{E}{F}}
\newcommand{\cmdctx}{D}

\newcommand{\enva}{\pick{\Gamma}{\Theta}}
\newcommand{\envb}{\pick{\Delta}{\Lambda}}
\newcommand{\coenva}{\dual{\enva}}
\newcommand{\coenvb}{\dual{\envb}}

\newcommand{\cmda}{S}
\newcommand{\cmdb}{T}

\newcommand{\typa}{A}
\newcommand{\typb}{B}
\newcommand{\typc}{C}
\newcommand{\typd}{A}
\newcommand{\type}{B}
\newcommand{\typx}{X}
\newcommand{\typr}{R}


% Continuation passing style translation

\newcommand{\cpstyp}[1]{\Tp{(\tp{#1})^\VN}}
\newcommand{\cpsval}[1]{\Tm{(\tm{#1})^\VN}}
\newcommand{\cpsexp}[1]{\Tm{(\tm{#1})^\vn}}
\newcommand{\cpscoexp}[1]{\Tm{(\tm{#1})^\vn}}
\newcommand{\cpscmd}[1]{\Tm{(\tm{#1})^\vn}}

\newcommand{\Cpstyp}[1]{\cpstyp{#1}}
\newcommand{\Cpsexp}[1]{\cpsexp{#1}}
\newcommand{\Cpsval}[1]{\cpsval{#1}}
\newcommand{\Cpscoexp}[1]{\cpscoexp{#1}}
\newcommand{\Cpscmd}[1]{\cpscmd{#1}}

\newcommand{\cpstypn}[1]{\dual{\cpstyp{\dual{#1}}}}
\newcommand{\cpsexpn}[1]{\dual{\cpsexp{\dual{#1}}}}
\newcommand{\cpsvaln}[1]{\dual{\cpsval{\dual{#1}}}}
\newcommand{\cpscoexpn}[1]{\dual{\cpscoexp{\dual{#1}}}}
\newcommand{\cpscmdn}[1]{\dual{\cpscmd{\dual{#1}}}}

\newcommand{\uncpstyp}[1]{\tp{(\Tp{#1})_\VN}}
\newcommand{\uncpsval}[1]{\tm{(\Tm{#1})_\VN}}
\newcommand{\uncpsexp}[1]{\tm{(\Tm{#1})_\vn}}
\newcommand{\uncpscoexp}[1]{\tm{(\Tm{#1})_\vn}}
\newcommand{\uncpscmd}[1]{\tm{(\Tm{#1})_\vn}}

\newcommand{\Uncpstyp}[1]{\uncpstyp{#1}}
\newcommand{\Uncpsexp}[1]{\uncpsexp{#1}}
\newcommand{\Uncpsval}[1]{\uncpsval{#1}}
\newcommand{\Uncpscoexp}[1]{\uncpscoexp{#1}}
\newcommand{\Uncpscmd}[1]{\uncpscmd{#1}}



% duality

\newcommand{\dualtyp}[1]{{#1}^\circ}
\newcommand{\dualenv}[1]{{#1}^\circ}
\newcommand{\dualseq}[1]{{#1}^\circ}
\newcommand{\dualcoenv}[1]{{#1}^\circ}
\newcommand{\dualexp}[1]{{#1}^\circ}
\newcommand{\dualcoexp}[1]{{#1}^\circ}
\newcommand{\dualcmd}[1]{{#1}^\circ}
\newcommand{\dualvar}[1]{{#1}^\circ}
\newcommand{\dualcovar}[1]{{#1}^\circ}

\newcommand{\Dualtyp}[1]{\dualtyp{(#1)}}
\newcommand{\Dualenv}[1]{\dualenv{(#1)}}
\newcommand{\Dualseq}[1]{\dualseq{(#1)}}
\newcommand{\Dualcoenv}[1]{\dualcoenv{(#1)}}
\newcommand{\Dualexp}[1]{\dualexp{(#1)}}
\newcommand{\Dualcoexp}[1]{\dualcoexp{(#1)}}
\newcommand{\Dualcmd}[1]{\dualcmd{(#1)}}

\newcommand{\doubledualtyp}[1]{{#1}^{\circ\circ}}
\newcommand{\doubledualexp}[1]{{#1}^{\circ\circ}}
\newcommand{\doubledualcoexp}[1]{{#1}^{\circ\circ}}
\newcommand{\doubledualcmd}[1]{{#1}^{\circ\circ}}
\newcommand{\doubledualvar}[1]{{#1}^{\circ\circ}}
\newcommand{\doubledualcovar}[1]{{#1}^{\circ\circ}}


% Girardian turnstyle

\newcommand{\headpiece}{\mathrel{\mkern-3mu\smash-}}
\newlength{\tailwidth}
\setlength{\tailwidth}{0.1em}
\newcommand{\tailpiece}[1]{\mathrel{\vrule height 1.4ex width #1\tailwidth depth .1ex}} 
\newcommand{\turnstyle}[1]{\mathrel{\tailpiece{#1}\headpiece}}

\newcommand{\exptail}{\tailpiece{1}}
\newcommand{\expturn}{\turnstyle{3}}
\newcommand{\cmdtail}{\tailpiece{2}}
\newcommand{\cmdturn}{\tailpiece{2}}

% judgements

\newcommand{\sep}{\mathrel{\jd{\mid}}}
\newcommand{\semi}{\jd{;}\;}
\newcommand{\comma}{\jd{,}\,}
\newcommand{\ellipses}{\jd{,\ldots,\,}}

\newcommand{\dec}[2]{\seqdual{\tp{#2}}{\tm{#1\,{:}\,\tp{#2}}}}
\newcommand{\Dec}[2]{\seqdual{\Tp{#2}}{\Tm{#1\,{:}\,\Tp{#2}}}}

\newcommand{\ext}[2]{\pick{#1 \comma #2}{#2 \comma #1}}
\newcommand{\coext}[2]{\dual{\ext{\dual{#2}}{\dual{#1}}}}

\newcommand{\sequentarrow}{\mbox{\ding{222}}}
\newcommand{\sequentmid}{\mbox{\ding{121}}}
\newcommand{\sequentmidarrow}{\sequentmid\!\sequentarrow}

\newcommand{\EXPJ}[4]{\tp{#1} \;\sequentarrow\; \tp{#4} \seqdual{,\,}{\:\sequentmid\:} \dec{#2}{#3}}
\newcommand{\COEXPJ}[4]{\dec{#2}{#3} \seqdual{,\,}{\:\sequentmid\:} \tp{#1} \;\sequentarrow\; \tp{#4}}
\newcommand{\CMDJ}[3]{\tp{#1} \seqdual{\;\sequentarrow\;}{\;\sequentmid\: \tm{#2} \:\sequentmidarrow\;} \tp{#3}}

\newcommand{\expj}[4]{\pick{\EXPJ{#1}{#2}{#3}{#4}}{\COEXPJ{#4}{#2}{#3}{#1}}}
\newcommand{\coexpj}[4]{\dual{\expj{\dual{#4}}{\dual{#2}}{\dual{#3}}{\dual{#1}}}}
\newcommand{\cmdj}[3]{\pick{\CMDJ{#1}{#2}{#3}}{\CMDJ{#3}{#2}{#1}}}

\newcommand{\seqj}[2]{\makesequent\cmdj{#1}{}{#2}}
\newcommand{\Expj}[3]{\Tp{#1} \;\sequentarrow\; \Dec{#2}{#3}}

\newcommand{\syntypej}[3]{\mbox{#1} & \tp{#2} &::=& \tp{#3}}
\newcommand{\synj}[3]{\mbox{#1} & \tm{#2} &::=& \tm{#3}}
\newcommand{\synjfirst}[3]{\mbox{#1} & \tm{#2} &::=& \tm{#3} \sep {}}
\newcommand{\synjnext}[1]{& & & \tm{#1} \sep {}}
\newcommand{\synjlast}[1]{& & & \tm{#1}}
\newcommand{\Syntypej}[3]{\mbox{#1} & \Tp{#2} &::=& \Tp{#3}}
\newcommand{\Synj}[3]{\mbox{#1} & \Tm{#2} &::=& \Tm{#3}}
\newcommand{\Synjfirst}[3]{\mbox{#1} & \Tm{#2} &::=& \Tm{#3} \sep {}}
\newcommand{\Synjnext}[1]{& & & \Tm{#1} \sep {}}
\newcommand{\Synjlast}[1]{& & & \Tm{#1}}
\newcommand{\synjsequent}[2]{\mbox{#1} & \multicolumn{3}{c}{#2}}

\newcommand{\redj}[3]{\tp{(#1)} & \tm{#2} &\tp{\becomes}& \tm{#3}}
\newcommand{\redjv}[3]{\tp{(#1)} & \tm{#2} &\tp{\becomesv}& \tm{#3}}
\newcommand{\redjn}[3]{\tp{(#1)} & \tm{#2} &\tp{\becomesn}& \tm{#3}}
\newcommand{\redjc}[3]{\tp{(#1)} & \tm{#2} &\tp{\becomes_c}& \tm{#3}}

\newcommand{\tranj}[2]{\tm{#1} &\defeq& \tm{#2}}
\newcommand{\trantypej}[2]{\tp{#1} &\defeqtype& \tp{#2}}
\newcommand{\Tranj}[2]{\Tm{#1} &\Defeq& \Tm{#2}}
\newcommand{\Trantypej}[2]{\Tp{#1} &\Defeqtype& \Tp{#2}}


% inference rules

\newcommand{\gap}{\hspace{2em}}
\newcommand{\samerule}{\hspace{2em}}
\newcommand{\sameline}{\hspace{3em}}
\newcommand{\nextline}{\\ \\}

\newcommand{\brule}{\prooftree}
\newcommand{\mrule}[1]{\using{#1}\justifies}
\newcommand{\erule}{\endprooftree}
\newcommand{\infer}[3]{\brule #1 \mrule{#2} #3 \erule}

\newcommand{\blankhole}{{\color{white}\hole}}
\newcommand{\hyp}[2]{\prooftree #1 \proofdotseparation=0.7ex\proofdotnumber=3\leadsto #2 \endprooftree}
\newcommand{\nohyp}[1]{\prooftree \proofdotseparation=0.7ex\proofdotnumber=3\leadsto #1 \endprooftree}

% connectives

\newcommand{\IFF}{~\mbox{iff}~}
\newcommand{\IMPLIES}{~\mbox{implies}~}

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

\newcommand{\thinningrule}{
 \infer{
   \cmdj{\enva}{\cmda}{\coenva}
 }{}{
   \cmdj{\ext{\dec{\vara}{\typd}}{\enva}}{\cmda}{\coenva}
 }
}

\newcommand{\thinningleftrule}{
 \infer{
   \expj{\enva}{\expa}{\typc}{\coenva}
 }{}{
   \expj{\ext{\dec{\vara}{\typd}}{\enva}}{\expa}{\typc}{\coenva}
 }
}

\newcommand{\thinningrightrule}{
 \infer{
   \expj{\enva}{\expa}{\typc}{\coenva}
 }{}{
   \expj{\coenva}{\expa}{\typc}{\ext{\coenva}{\dec{\covara}{\typd}}}
 }
}

\newcommand{\contractionrule}{
 \infer{
   \cmdj{\ext{\ext{\dec{\vara}{\typd}}{\dec{\varb}{\typd}}}{\enva}}{\cmda}{\coenva}
 }{}{
   \cmdj{\ext{\dec{\vara}{\typd}}{\enva}}{\sub{\cmda}{\vara}{\varb}}{\coenva}
 }
}

\newcommand{\contractionleftrule}{
 \infer{
   \expj{\ext{\ext{\dec{\vara}{\typd}}{\dec{\varb}{\typd}}}{\enva}}{\expa}{\typc}{\coenva}
 }{}{
   \expj{\ext{\dec{\vara}{\typd}}{\enva}}{\sub{\expa}{\vara}{\varb}}{\typc}{\coenva}
 }
}

\newcommand{\contractionrightrule}{
 \infer{
   \expj{\enva}{\expa}{\typc}{\ext{\coenva}{\ext{\dec{\covarb}{\typd}}{\dec{\covara}{\typd}}}}
 }{}{
   \expj{\enva}{\sub{\expa}{\covara}{\covarb}}{\typc}{\ext{\coenva}{\dec{\covara}{\typd}}}
 }
}

\newcommand{\interchangerule}{
 \infer{
   \cmdj{\ext{\envb}{\ext{\ext{\dec{\vara}{\typd}}{\dec{\varb}{\type}}}{\enva}}}{\cmda}{\coenva}
 }{}{
   \cmdj{\ext{\envb}{\ext{\ext{\dec{\varb}{\type}}{\dec{\vara}{\typd}}}{\enva}}}{\cmda}{\coenva}
 }
}

\newcommand{\interchangeleftrule}{
 \infer{
   \expj{\ext{\envb}{\ext{\ext{\dec{\vara}{\typd}}{\dec{\varb}{\type}}}{\enva}}}{\expa}{\typc}{\coenva}
 }{}{
   \expj{\ext{\envb}{\ext{\ext{\dec{\varb}{\type}}{\dec{\vara}{\type}}}{\enva}}}{\expa}{\typc}{\coenva}
 }
}

\newcommand{\interchangerightrule}{
 \infer{
   \expj{\enva}{\expa}{\typc}{\ext{\ext{\coenva}{\ext{\dec{\covarb}{\type}}{\dec{\covara}{\typd}}}}{\coenvb}}
 }{}{
   \expj{\enva}{\expa}{\typc}{\ext{\ext{\coenva}{\ext{\dec{\covara}{\typd}}{\dec{\covarb}{\type}}}}{\coenvb}}
 }
}


\newcommand{\idrule}{
 \infer{
 }{\Id}{
  \cmdj{\dec{\vara}{\typd}}{\cut{\vara}{\covara}}{\dec{\covara}{\typd}}
 }
}

\newcommand{\idrightrule}{
 \infer{
 }{\Id\Right}{
  \expj{\dec{\vara}{\typd}}{\vara}{\typd}{\,}
 }
}

\newcommand{\pairrule}{
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \expj{\enva}{\expb}{\typb}{\coenva}
 }{\And\Right}{
  \expj{\enva}{\pair{\expa}{\expb}}{\typa \And \typb}{\coenva}
 }
}

\newcommand{\fstrule}{
 \infer{
  \coexpj{\enva}{\coexpa}{\typa}{\coenva}
 }{}{
  \coexpj{\enva}{\fst{\coexpa}}{\typa \And \typb}{\coenva}
 }
}

\newcommand{\sndrule}{
 \infer{
  \coexpj{\enva}{\coexpb}{\typb}{\coenva}
 }{\And\Left}{
  \coexpj{\enva}{\snd{\coexpb}}{\typa \And \typb}{\coenva}
 }
}

\newcommand{\notrule}{
 \infer{
  \coexpj{\enva}{\coexpa}{\typa}{\coenva}
 }{\Not\Right}{
  \expj{\enva}{\comp{\coexpa}}{\Not\typa}{\coenva}
 }
}

\newcommand{\impliesrightrule}{
 \infer{
  \expj{\ext{\dec{\vara}{\typa}}{\enva}}{\expb}{\typb}{\coenva}
 }{\Implies\Right}{
  \expj{\enva}{\dualabs{\vara}{\expb}}{\typa \Implies \typb}{\coenva}
 }
}

\newcommand{\impliesleftrule}{
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \coexpj{\envb}{\coexpb}{\typb}{\coenvb}
 }{\Implies\Left}{
  \coexpj{\ext{\enva}{\envb}}{\dualapp{\expa}{\coexpb}}{\typa \Implies \typb}{\ext{\coenva}{\coenvb}}
 }
}

\newcommand{\cobindrule}{
 \infer{
  \cmdj{\enva}{\cmda}{\coext{\coenva}{\dec{\covara}{\typa}}}
 }{\Right\Intro}{
  \expj{\enva}{\cobind{\cmda}{\covara}}{\typa}{\coenva}
 }
}

\newcommand{\cutrule}{
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \coexpj{\envb}{\coexpa}{\typa}{\coenvb}
 }{\Cut}{
  \cmdj{\ext{\enva}{\envb}}{\cut{\expa}{\coexpa}}{\ext{\coenva}{\coenvb}}
 }
}

\newcommand{\dualabsrule}{
 \infer{
  \expj{\ext{\dec{\vara}{\typa}}{\enva}}{\expb}{\typb}{\coenva}
 }{\Implies\Right}{
  \expj{\enva}{\dualabs{\vara}{\expb}}{\typa \Implies \typb}{\coenva}
 }
}

\newcommand{\dualapprule}{
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \coexpj{\enva}{\coexpb}{\typb}{\coenva}
 }{\Implies\Left}{
  \coexpj{\enva}{\dualapp{\expa}{\coexpb}}{\typa \Implies \typb}{\coenva}
 }
}

\newcommand{\cobindelimrule}{
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 }{\Right\Elim}{
  \cmdj{\enva}{\cut{\expa}{\covara}}{\ext{\coenva}{\dec{\covara}{\typa}}}
 }
}

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

\newcommand{\naturalrules}{
\begin{rules}
\infer
  {\nohyp{\dec{M}{A}}\quad\nohyp{\dec{N}{B}}}
  {\And\Intro}
  {\dec{(M,N)}{A \And B}}
\quad\quad
\infer
  {\nohyp{\dec{O}{A \And B}}}
  {}
  {\dec{\tfst{O}}{A}}
\quad
\infer
  {\nohyp{\dec{O}{A \And B}}}
  {\And\Elim}
  {\dec{\tsnd{O}}{B}}
\\ \\
\infer
  {\hyp{\blankhole}{\dec{M}{A}}}
  {}
  {\dec{\tinl{M}}{A \Or B}}
\quad
\infer
  {\hyp{\blankhole}{\dec{N}{B}}}
  {\Or\Intro}
  {\dec{\tinr{N}}{A \Or B}}
\quad\quad
\infer
  {\hyp{\blankhole}{\dec{O}{A \Or B}} \quad
   \hyp{\fillhole{\dec{x}{A}}}{\dec{P}{C}} \quad
   \hyp{\fillhole{\dec{y}{B}}}{\dec{Q}{C}}}
  {\Or\Elim}
  {\dec{\sumcase{O}{x}{P}{y}{Q}}{C}}
\\ \\
\infer
  {\hyp{\fillhole{\dec{x}{A}}}{\dec{N}{B}}}
  {\Implies\Intro}
  {\dec{\abs{x}{N}}{A \Implies B}}
\quad\quad
\infer
  {\hyp{\blankhole}{\dec{O}{A \Implies B}} \quad \hyp{\blankhole}{\dec{M}{A}}}
  {\Implies\Elim}
  {\dec{O\app{M}}{B}}
\end{rules}
}


\newcommand{\naturalreductions}{
\begin{rules}
\infer
 {\infer
   {\nohyp{\dec{M}{A}} \quad \nohyp{\dec{N}{B}}}
   {\And\Intro}
   {\dec{(M,N)}{A \And B}}}
 {\And\Elim}
 {\dec{\tfst{(M,N)}}{A}}
~~\longrightarrow~~
\nohyp{\dec{M}{A}}

\\ \\

\infer
 {\infer
   {\nohyp{\dec{M}{A}}}
   {\Or\Intro}
   {\dec{\tinl{M}}{A \Or B}}
  \quad\hyp{\fillhole{\dec{x}{A}}}{\dec{P}{C}}
  \quad\hyp{\fillhole{\dec{y}{B}}}{\dec{Q}{C}}} 
 {\Or\Elim}
 {\dec{\sumcase{(\tinl{M})}{x}{P}{y}{Q}}{C}}
~~\longrightarrow~~
\hyp{\nohyp{\dec{M}{A}}}{\dec{\sub{P}{M}{x}}{C}}

\\ \\

\infer
 {\infer
   {\hyp{\fillhole{\dec{x}{A}}}{\dec{N}{B}}}
   {\Implies\Intro}
   {\dec{\abs{x}{N}}{A \Implies B}}
  \quad\nohyp{\dec{M}{A}}}
 {\Implies\Elim}
 {\dec{(\abs{x}{N})\app{M}}{B}}
~~\longrightarrow~~
\hyp{\nohyp{\dec{M}{A}}}{\dec{\sub{N}{M}{x}}{B}}

\end{rules}
}


\newcommand{\cutelimination}{
\begin{rules}
\infer{
  \infer{
   \expj{\enva}{\expa}{\typa}{\coenva}
  \gap
   \expj{\enva}{\expb}{\typb}{\coenva}
  }{\And\Right}{
   \expj{\enva}{\pair{\expa}{\expb}}{\typa \And \typb}{\coenva}
  }
  \gap
 \infer{
  \coexpj{\enva}{\coexpa}{\typa}{\coenva}
 }{\And\Left}{
  \coexpj{\enva}{\fst{\coexpa}}{\typa \And \typb}{\coenva}
 }
}{\Cut}{
  \cmdj{\enva}{\cut{\pair{\expa}{\expb}}{\fst{\coexpa}}}{\coenva}
}
\\ \vspace{-1ex} \\
\longrightarrow~~~~
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \coexpj{\enva}{\coexpa}{\typa}{\coenva}
 }{\Cut}{
  \cmdj{\enva}{\cut{\expa}{\coexpa}}{\coenva}
 }

\\ \\ \\

\infer{
  \infer{
   \coexpj{\enva}{\coexpa}{\typa}{\coenva}
  }{\Not\Right}{
   \expj{\enva}{\comp{\coexpa}}{\Not\typa}{\coenva}
  }
  \gap
  \dual{
    \infer{
     \coexpj{\enva}{\coexpa}{\typa}{\coenva}
    }{\Not\Right}{
     \expj{\enva}{\comp{\coexpa}}{\Not\typa}{\coenva}
    }
  }
}{\Cut}{
  \cmdj{\enva}{\cut{\comp{\coexpa}}{\cocomp{\expa}}}{\coenva}
}
\\ \vspace{-1ex} \\
\longrightarrow~~~~
 \infer{
  \expj{\enva}{\expa}{\typa}{\coenva}
 \gap
  \coexpj{\enva}{\coexpa}{\typa}{\coenva}
 }{\Cut}{
  \cmdj{\enva}{\cut{\expa}{\coexpa}}{\coenva}
 }

\end{rules}
}


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

\newcommand{\photo}[3]{
  \begin{tabular}{c}
  \scalebox{#1}{\includegraphics{#2}} \\
  #3
  \end{tabular}
}

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

\begin{document}



\titleslide
  {Call-by-name is dual to call-by-value}
  {Philip Wadler\\ University of Edinburgh\\ wadler@inf.ed.ac.uk}


\partslide{A Deal with the Devil}


\begin{centerslide}\Large
Either \\
(a) I will give you \$1,000,000,000 \\
or \\
(b) I will grant you one wish if you pay me \$1,000,000,000.
\end{centerslide}


\begin{centerslide}\Large
Either \\
(a) I will give you \$1,000,000,000 \\
or \\
\blue{(b) I will grant you one wish if you pay me \$1,000,000,000.}
\end{centerslide}


\begin{centerslide}\Large
Either \\
\blue{(a) I will give you \$1,000,000,000} \\
or \\
(b) I will grant you one wish if you pay me \$1,000,000,000.
\end{centerslide}


\partslide{A Question}


\begin{centerslide}
\[\Large
\frac{\blue{\textrm{Lambda Calculus}}}
     {\ba{c}\blue{\textrm{Natural Deduction}}\\ \blue{\textrm{(Intuitonistic)}}\ea}
~~=~~
\frac{\blue{\textrm{?}}}
     {\ba{c}\blue{\textrm{Sequent Calculus}} \\ \blue{\textrm{(Classical)}}\ea}
\]
\end{centerslide}


\begin{centerslide}
\[\Large
\frac{\blue{\textrm{Lambda Calculus}}}
     {\ba{c}\blue{\textrm{Natural Deduction}}\\ \blue{\textrm{(Intuitonistic)}}\ea}
~~=~~
\frac{\blue{\textrm{Dual Calculus}}}
     {\ba{c}\blue{\textrm{Sequent Calculus}} \\ \blue{\textrm{(Classical)}}\ea}
\]
\end{centerslide}


\partslide{The History}


\begin{Slide}{Logic}
\begin{center}
\photo{0.32}{images/Boole-portrait.jpg}{George Boole (1815--1864)}
\quad
\photo{0.24}{images/Frege-portrait.jpg}{Gottlob Frege (1848--1925)}
\end{center}
\\
\begin{center}
\blue{Boole (1847): }\emph{Laws of Thought}  \\[1ex]
\blue{Frege (1879): }\emph{Begriffsschrift} 
\end{center}
\end{Slide}


\begin{Slide}{Duality}
\\
\newcommand{\consistencylaw}{
 \tp{\typa \And \Not\typa} = \tp{\Bot}
}
\newcommand{\distlaw}{
 \tp{\typa \And (\typb \Or \typc)}
 =
 \tp{(\typa \And \typb) \Or (\typa \And \typc)}
}
\begin{rules}
 \consistencylaw \\
 \dual{\consistencylaw} \\ \\
 \distlaw \\
 \dual{\distlaw} 
\end{rules}
\\
\begin{center}
\blue{Poncelet (1818), Gergonne (1826): }duals in projective geometry \\[1ex]
\blue{Boole (1847), Frege (1879): }no duality!  \\[1ex]
\blue{Schr\"oder (1890): }duals in logic
\end{center}
\end{Slide}


\begin{Slide}{Natural Deduction and Lambda Calculus}
\begin{center}
\photo{0.2}{images/Church-photo.jpg}{Alonzo Church (1903--1995)}
\quad
\photo{0.2}{images/Gentzen-photo.jpg}{Gerhard Gentzen (1909--1945)}
\end{center}
\\
\begin{center}
\blue{Church (1932): }$\lambda$-calculus  \\[1ex]
\blue{Gentzen (1935): }natural deduction  \\[1ex]
\blue{Church (1940): }simply-typed $\lambda$-calculus  \\[1ex]
\end{center}
\end{Slide}


\begin{Slide}{The Curry-Howard Isomorphism}
\begin{center}
\photo{0.32}{images/Curry-portrait.jpg}{Haskell Curry (1900--1982)}
\quad
\photo{0.72}{images/Howard-portrait.jpg}{William Howard}
\end{center}
\\
\begin{center}
\blue{Curry and Feys (1958): }combinatory logic  \\[1ex]
\blue{Prawitz (1965): }proof reduction  \\[1ex]
\blue{de Bruijn (1968): }encoding of proofs  \\[1ex]
\blue{Howard (1980): }natural deduction $\simeq$ $\lambda$-calculus
\end{center}
\end{Slide}


\begin{Slide}{Curry-Howard for Classical Logic}
\\
\begin{center}
\blue{Gentzen (1935): }sequent calculus  \\[1ex]
\blue{Filinski (1989): }symmetric $\lambda$-calculus \\[1ex]
\blue{Griffin (1990): }Curry-Howard for classical logic \\[1ex]
\blue{Parigot (1992): }$\lambda\mu$-calculus \\[1ex]
\blue{Danos, Joinet, and Schellinx (1995): }dual encodings in linear logic \\[1ex]
\blue{Barbanera and Berardi (1996): }symmetric $\lambda$-calculus \\[1ex]
\blue{Streicher and Reus (1998): }dual cps transforms \\[1ex]
\blue{Selinger (1998): }dual control categories \\[1ex]
\blue{Curien and Herbelin (2000): }Curry-Howard for classical sequent calculus \\[1ex]
\blue{Wadler (2003): }dual calculus
\end{center}
\end{Slide}


\partslide{Natural Deduction \\ (Intuitionistic)}


\imageslide
  {Gentzen 1935: Natural Deduction}
  {0.8}{images/gentzen-77.jpg}


\begin{Slide}{Gentzen 1935: Natural Deduction}
\makesequent
\naturalrules
\end{Slide}


\begin{Slide}{Prawitz 1965: Simplifying proofs}
\makesequent
\naturalreductions
\end{Slide}


\partslide{The Lambda Calculus}


\imageslide
  {Church 1932: Lambda Calculus}
  {0.7}{images/church-352.jpg}


\begin{Slide}{Church 1940: Simply-typed Lambda Calculus}
\makedual
\naturalrules
\end{Slide}


\begin{Slide}{Church 1932, 1940: Reducing terms}
\makedual
\naturalreductions
\end{Slide}


\begin{Slide}{Church 1932: Call-by-name}
\\
 \begin{reductions}
  \redjn{\beta\And}
    {\tfst{(M,N)}}
    {M} \\
  \redjn{\beta\And}
    {\tsnd{(M,N)}}
    {N}  \\
  \redjn{\beta\Or}
    {\sumcase{(\tinl{M})}{x}{P}{y}{Q}}
    {\sub{P}{M}{x}}  \\
  \redjn{\beta\Or}
    {\sumcase{(\tinr{N})}{x}{P}{y}{Q}}
    {\sub{Q}{N}{y}}  \\
  \redjn{\beta\Implies}
    {(\abs{x}{N})\app{M}}
    {\sub{N}{M}{x}}
 \end{reductions}
\end{Slide}



\begin{Slide}{Rosser 1936, Plotkin 1975: Call-by-value}
\\
 \begin{syntax}
  \synj{\blue{Value}}{V,W}{x \sep (V,W) \sep \tinl{V} \sep \tinr{W} \sep \abs{x}{N}}
 \end{syntax}
 \begin{reductions}
  \redjv{\beta\And}
    {\tfst{(V,W)}}
    {V} \\
  \redjv{\beta\And}
    {\tsnd{(V,W)}}
    {W}  \\
  \redjv{\beta\Or}
    {\sumcase{\tinl{V}}{x}{P}{y}{Q}}
    {\sub{P}{V}{x}}  \\
  \redjv{\beta\Or}
    {\sumcase{\tinr{W}}{x}{P}{y}{Q}}
    {\sub{Q}{W}{y}}  \\
  \redjv{\beta\Implies}
    {(\abs{x}{N})\app{V}}
    {\sub{N}{V}{x}}
 \end{reductions}
\end{Slide}



\partslide{Sequent Calculus \\ (Classical)}


\imageslide
  {Gentzen 1935: Sequent Calculus}
  {0.8}{images/gentzen-84.jpg}


\begin{Slide}{Gentzen 1935: Logical rules}
\makesequent
\begin{rules}
\pairrule \nextline
\fstrule \samerule \sndrule
\nextline
\dual{\fstrule \samerule \sndrule}
\nextline
\dual{\pairrule}
\nextline
\notrule \sameline \dual{\notrule}
\end{rules}
\end{Slide}


\begin{Slide}{Gentzen 1935: Structural rules}
\makesequent
\begin{rules}
\idrule
\nextline
\cutrule
\end{rules}
\end{Slide}


\begin{Slide}{Gentzen 1935: Duality}
\\
\begin{translation}
  \trantypej{\Dualtyp{\typx}}
   {\typx} \\
  \trantypej{\Dualtyp{\typa \And \typb}}
   {\dualtyp{\typa} \Or \dualtyp{\typb}} \\
  \trantypej{\Dualtyp{\typa \Or \typb}}
   {\dualtyp{\typa} \And \dualtyp{\typb}} \\
  \trantypej{\Dualtyp{\Not\typa}}
   {\Not\dualtyp{\typa}}
\end{translation}
\begin{translation}
  \trantypej{\Dualtyp{A_1,\ldots,A_n}}
   {\dualtyp{A}_n,\ldots,\dualtyp{A}_1}
\end{translation}
\\
\begin{proposition}
A sequent is derivable if and only if its dual is derivable,
\[\colored
 \seqj{\enva}{\coenva} \quad\mbox{iff}\quad \seqj{\dualtyp{\coenva}}{\dualtyp{\enva}}.
\]
\end{proposition}
\end{Slide}


\begin{Slide}{Gentzen 1935: Cut Elimination}
\\
\makesequent
\cutelimination
\end{Slide}


\partslide{The dual calculus}


\newcommand{\longenva}{\dec{\vara_1}{\typa_1} \ellipses \dec{\vara_m}{\typa_m}}
\newcommand{\longcoenva}{\dec{\covara_1}{\typb_1} \ellipses \dec{\covara_n}{\typb_n}}


\begin{Slide}{Intuitionistic natural deduction}
\\
 \begin{syntax}%
  \synjsequent{Term}{\longenva \;\sequentarrow\; \dec{\expa}{\typa}}
 \end{syntax}%
\\
\\
\slidetitle{Classical sequent calculus}
\\
 \begin{syntax}%
  \synjsequent{Term}{\expj{\longenva}{\expa}{\typa}{\longcoenva}} \\[1ex]
  \synjsequent{Coterm}{\coexpj{\longenva}{\coexpa}{\typa}{\longcoenva}} \\[1ex]
  \synjsequent{Statement}{\cmdj{\longenva}{\cmda}{\longcoenva}}
 \end{syntax}%
\end{Slide}


\begin{Slide}{Terms, Coterms, Statements}
\\ \\
 \[\colored\ba{@{}lccc@{\,|\,}c@{\,|\,}c@{\,|\,}c@{\,|\,}c@{\,|\,}c}
  \mbox{Term} & \tm{\expa,\expb} &::=&
   \tm{\vara} & \tm{\pair{\expa}{\expb}} & \tm{\inl{\expa}} & \tm{\inr{\expb}}
         & \tm{\comp{\coexpa}} & \tm{\cobind{\cmda}{\covara}} \\
  \mbox{Coterm} & \tm{\coexpa,\coexpb} &::=&
   \tm{\covara} & \tm{\case{\coexpa}{\coexpb}} & \tm{\fst{\coexpa}} & \tm{\snd{\coexpb}}
           & \tm{\cocomp{\expa}} & \tm{\bind{\vara}{\cmda}} \\
  \mbox{Statement} & \tm{\cmda,\cmdb} &::=&
   \multicolumn{6}{l}{\tm{\cut{\expa}{\coexpa}}}
 \ea\]
\\ \\
 \begin{syntax}%
  \synjsequent{Right sequent}{\expj{\enva}{\expa}{\typa}{\coenva}} \\
  \synjsequent{Left sequent}{\coexpj{\enva}{\coexpa}{\typa}{\coenva}} \\
  \synjsequent{Center sequent}{\cmdj{\enva}{\cmda}{\coenva}}
 \end{syntax}%
\end{Slide}


\begin{Slide}{Logical rules}
\begin{rules}
\pairrule \nextline
\fstrule \samerule \sndrule
\nextline
\dual{\fstrule \samerule \sndrule}
\nextline
\dual{\pairrule}
\nextline
\notrule \sameline \dual{\notrule}
\end{rules}
\end{Slide}


\begin{Slide}{Structural rules}
\\
\begin{rules}
\idrightrule \sameline \dual{\idrightrule}
\nextline
\cobindrule \sameline \dual{\cobindrule}
\nextline
\cutrule
\end{rules}
\end{Slide}


\begin{Slide}{Duality}
 \quadruple{
  \trantypej{\Dualtyp{\typx}}
   {\typx} \\
  \trantypej{\Dualtyp{\typa \And \typb}}
   {\dualtyp{\typa} \Or \dualtyp{\typb}} \\
  \trantypej{\Dualtyp{\typa \Or \typb}}
   {\dualtyp{\typa} \And \dualtyp{\typb}} \\
  \trantypej{\Dualtyp{\Not\typa}}
   {\Not\dualtyp{\typa}}
 }{
  \tranj{\Dualexp{\vara}}
   {\dualvar{\vara}} \\
  \tranj{\Dualexp{\pair{\expa}{\expb}}}
   {\case{\dualexp{\expa}}{\dualexp{\expb}}} \\
  \tranj{\Dualexp{\inl{\expa}}}
   {\fst{\dualexp{\expa}}} \\
  \tranj{\Dualexp{\inr{\expb}}}
   {\snd{\dualexp{\expa}}} \\
  \tranj{\Dualexp{\comp{\coexpa}}} 
   {\cocomp{\dualcoexp{\coexpa}}} \\
  \tranj{\Dualexp{\cobind{\cmda}{\covara}}}
   {\bind{\dualcovar{\covara}}{\dualcmd{\cmda}}}
 }{
  \tranj{\Dualcoexp{\covara}}
   {\dualvar{\covara}}  \\
  \tranj{\Dualcoexp{\case{\coexpa}{\coexpb}}}
   {\pair{\dualcoexp{\coexpa}}{\dualcoexp{\coexpb}}} \\
  \tranj{\Dualcoexp{\fst{\coexpa}}}
   {\inl{\dualcoexp{\coexpa}}} \\
  \tranj{\Dualcoexp{\snd{\coexpb}}}
   {\inr{\dualcoexp{\coexpa}}} \\
  \tranj{\Dualcoexp{\cocomp{\expa}}}
   {\comp{\dualexp{\expa}}} \\
  \tranj{\Dualcoexp{\bind{\vara}{\cmda}}}
   {\cobind{\dualcmd{\cmda}}{\dualvar{\vara}}}
 }{
  \tranj{\Dualcmd{\cut{\expa}{\coexpa}}}
   {\cut{\dualcoexp{\coexpa}}{\dualexp{\expa}}}
 }
\end{Slide}


\begin{Slide}{Duality}
\\
\begin{proposition}
A sequent is derivable if and only if its dual is derivable,
\[\colored
\left.
\ba{r}
\expj{\enva}{\expa}{\typa}{\coenva} \\
\coexpj{\enva}{\coexpa}{\typa}{\coenva} \\
\cmdj{\enva}{\cmda}{\coenva}
\ea
\right\}
\IFF
\left\{
\ba{l}
\coexpj{\dualcoenv{\coenva}}{\dualexp{\expa}}{\dualtyp{\typa}}{\dualenv{\enva}} \\
\expj{\dualcoenv{\coenva}}{\dualcoexp{\coexpa}}{\dualtyp{\typa}}{\dualenv{\enva}} \\
\cmdj{\dualcoenv{\coenva}}{\dualcmd{\cmda}}{\dualenv{\enva}}.
\ea
\right.
\]
\end{proposition}
\end{Slide}


\begin{Slide}{Gentzen (1935): Cut Elimination}
\\
\makedual
\cutelimination
\end{Slide}


\partslide{Call-by-value is Dual to Call-by-name}


\begin{Slide}{Critical pair}
\begin{reductions}%
 \redj{\beta\Left}
  {\cut{\expa}{\bind{\vara}{\cmda}}}
  {\sub{\cmda}{\expa}{\vara}} \\
 \redj{\beta\Right}
  {\cut{\cobind{\cmda}{\covara}}{\coexpa}}
  {\sub{\cmda}{\coexpa}{\covara}}
\end{reductions}%
Sometimes confluent.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\bind {\varb}{\cut {\varb}{\covarb}}}} \\
\tp{\swarrow} \quad\quad\quad\quad \tp{\searrow} \\
\tm{\cut{\vara}{\bind{\varb}{\cut{\varb}{\covarb}}}}
\quad\quad\quad
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\covarb}} \\
\tp{\searrow} \quad\quad\quad\quad \tp{\swarrow} \\
\tm{\cut{\vara}{\covarb}}
\end{rules}%
Sometimes not.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covarb}}{\bind{\varb}{\cut{\varc}{\covarc}}}} \\
\tp{\swarrow} \quad\quad\quad\quad \tp{\searrow} \\
\tm{\cut{\vara}{\covara}} \quad\quad\quad\quad\quad \tm{\cut{\varc}{\covarc}}
\end{rules}%
\end{Slide}


\begin{Slide}{Call-by-value}
\begin{reductions}%
 \redj{\beta\Left}
  {\cut{\vala}{\bind{\vara}{\cmda}}}
  {\sub{\cmda}{\vala}{\vara}} \\
 \redj{\beta\Right}
  {\cut{\cobind{\cmda}{\covara}}{\coexpa}}
  {\sub{\cmda}{\coexpa}{\covara}}
\end{reductions}%
Sometimes confluent.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\bind {\varb}{\cut {\varb}{\covarb}}}} \\
\tp{\swarrow} \quad\quad\quad\quad \white{\searrow} \\
\tm{\cut{\vara}{\bind{\varb}{\cut{\varb}{\covarb}}}}
\quad\quad\quad
\white{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\covarb}} \\
\tp{\searrow} \quad\quad\quad\quad \white{\swarrow} \\
\tm{\cut{\vara}{\covarb}}
\end{rules}%
Sometimes not.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covarb}}{\bind{\varb}{\cut{\varc}{\covarc}}}} \\
\tp{\swarrow} \quad\quad\quad\quad \white{\searrow} \\
\tm{\cut{\vara}{\covara}} \quad\quad\quad\quad\quad \white{\cut{\varc}{\covarc}}
\end{rules}%
\end{Slide}


\begin{Slide}{Call-by-name}
\begin{reductions}%
 \redj{\beta\Left}
  {\cut{\expa}{\bind{\vara}{\cmda}}}
  {\sub{\cmda}{\expa}{\vara}} \\
 \redj{\beta\Right}
  {\cut{\cobind{\cmda}{\covara}}{\covala}}
  {\sub{\cmda}{\covala}{\covara}}
\end{reductions}%
Sometimes confluent.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\bind {\varb}{\cut {\varb}{\covarb}}}} \\
\white{\swarrow} \quad\quad\quad\quad \tp{\searrow} \\
\white{\cut{\vara}{\bind{\varb}{\cut{\varb}{\covarb}}}}
\quad\quad\quad
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covara}}{\covarb}} \\
\white{\searrow} \quad\quad\quad\quad \tp{\swarrow} \\
\tm{\cut{\vara}{\covarb}}
\end{rules}%
Sometimes not.
\begin{rules}%
\tm{\cut{\cobind{\cut{\vara}{\covara}}{\covarb}}{\bind{\varb}{\cut{\varc}{\covarc}}}} \\
\white{\swarrow} \quad\quad\quad\quad \tp{\searrow} \\
\white{\cut{\vara}{\covara}} \quad\quad\quad\quad\quad \tm{\cut{\varc}{\covarc}}
\end{rules}%
\end{Slide}


\twice{

\begin{Slide}{Call-by-\pick{value}{name} reductions}
 \begin{syntax}
  \synj{\blue{\pick{Value}{Covalue}}}{\vala,\valb}
   {\vara \sep \pair{\vala}{\valb} \sep \inl{\vala} \sep \inr{\valb}
          \sep \comp{\coexpa}}
 \end{syntax}
 \begin{reductions}
  \redjv{\beta\And}
    {\cut{\pair{\vala}{\valb}}{\fst{\coexpa}}}
    {\cut{\vala}{\coexpa}} \\
  \redjv{\beta\And}
    {\cut{\pair{\vala}{\valb}}{\snd{\coexpb}}}
    {\cut{\valb}{\coexpb}} \\
  \redjv{\beta\Or}
    {\cut{\inl{\vala}}{\case{\coexpa}{\coexpb}}}
    {\cut{\vala}{\coexpa}} \\
  \redjv{\beta\Or}
    {\cut{\inr{\valb}}{\case{\coexpa}{\coexpb}}}
    {\cut{\valb}{\coexpb}} \\
  \redjv{\beta\Not}
   {\cut{\comp{\coexpa}}{\cocomp{\expa}}}{\cut{\expa}{\coexpa}} \\
  \redjv{\beta\Left}
   {\cut{\vala}{\bind{\vara}{\cmda}}}
   {\sub{\cmda}{\vala}{\vara}} \\
  \redjv{\beta\Right}
   {\cut{\cobind{\cmda}{\covara}}{\coexpa}}
   {\sub{\cmda}{\coexpa}{\covara}}
 \end{reductions}
\end{Slide}

}  %%% end twice


\twice{

\begin{Slide}{Call-by-\pick{value}{name}, additional reductions}
 \begin{syntax}
  \synj{\pick{Term}{Coterm} context}{\expctx}
   {\pair{\hole}{\expa} \sep \pair{\vala}{\hole} \sep \inl{\hole} \sep \inr{\hole}}
 \end{syntax}
 \begin{reductions}
  \redjv{\eta\Left}
   {\coexpa}
   {\bind{\vara}{\cut{\vara}{\coexpa}}}  \\
  \redjv{\eta\Right}
   {\expa}
   {\cobind{\cut{\expa}{\covara}}{\covara}}  \\
  \redjv{\varsigma}
   {\expctx\fillhole{\expa}}
   {\cobind{\cut{\expa}{\bind{\vara}{\cut{\expctx\fillhole{\vara}}{\covarb}}}}{\covarb}}
 \end{reductions}
\end{Slide}

}  %%% end twice


\begin{Slide}{Call-by-value is dual to call-by-name}
\\ \\
\begin{proposition}
Call-by-value is dual to call-by-name,
\[\colored
\left.
\ba{r}
\tm{\expa} \becomesv \tm{\expb} \\
\tm{\coexpa} \becomesv \tm{\coexpb} \\
\tm{\cmda} \becomesv \tm{\cmdb}
\ea
\right\}
\IFF
\left\{
\ba{l}
\tm{\dualexp{\expa}} \becomesn \tm{\dualexp{\expb}} \\
\tm{\dualexp{\coexpa}} \becomesn \tm{\dualexp{\coexpb}} \\
\tm{\dualexp{\cmda}} \becomesn \tm{\dualexp{\cmdb}}.
\ea
\right.
\]
\end{proposition}
\end{Slide}


\partslide{Excluded middle}


\begin{Slide}{Excluded middle}
\begin{rules}%
\infer
  {\infer
    {\infer
      {\infer
          {\infer
            {\infer
              {\infer
                {\infer
                    {\infer
                      {}
                      {\Id\Right}
                      {\expj
                      {\dec {x} {A}}
                      {x}
                      {A}
                      {\!}}}
                    {\Or\Right}
                    {\expj
                      {\dec {x} {A}}
                      {\inl {x}}
                      {A \Or \Not {A}}
                      {\!}}}
                {\Right\Elim}
                {\cmdj
                  {\dec {x} {A}}
                  {\cut {\inl {x}} {\gamma}}
                  {\dec {\gamma} {A \Or \Not {A}}}}}
              {\Left\Intro}
              {\coexpj
                {\!}
                {\bind {x} {\cut {\inl {x}} {\gamma}}}
                {A}
                {\dec {\gamma} {A \Or \Not {A}}}}}
            {\Not\Right}
            {\expj
              {}
              {\comp {\bind {x} {\cut {\inl {x}} {\gamma}}}}
              {\Not {A}}
              {\dec {\gamma} {A \Or \Not {A}}}}}
          {\Or\Right}
          {\expj
            {}
            {\inr {\comp {\bind {x} {\cut {\inl {x}} {\gamma}}}}}
            {A \Or \Not {A}}
            {\dec {\gamma} {A \Or \Not {A}}}}}
      {\Right\Elim}
      {\cmdj
        {}
        {\cut {\inr {\comp {\bind {x} {\cut {\inl {x}} {\gamma}}}}} {\delta}}
        {\ext {\dec {\gamma} {A \Or \Not {A}}} {\dec {\delta} {A \Or \Not {A}}}}}}
    {\mbox{Cont}}
    {\cmdj
      {}
      {\cut {\inr {\comp {\bind {x} {\cut {\inl {x}} {\gamma}}}}} {\gamma}}
      {\dec {\gamma} {A \Or \Not {A}}}}}
  {\Right\Intro}
  {\expj
    {}
    {\cobind {\cut {\inr {\comp {\bind {x} {\cut {\inl {x}} {\gamma}}}}} {\gamma}} {\gamma}}
    {A \Or \Not {A}}
    {\!}}
\end{rules}%
\end{Slide}


\partslide{Functions}


\begin{Slide}{Encoding functions in call-by-value}
\\  \\
\begin{rules}
\dualabsrule \sameline \dualapprule
\end{rules}
\begin{reductions}
  \redjv{\beta\Implies}
   {\cut{\dualabs{\vara}{\expb}}{\dualapp{\vala}{\coexpb}}}
   {\cut{\vala}{\bind{\vara}{\cut{\expb}{\coexpb}}}} \\
\end{reductions}
\\
 \begin{proposition} Under call-by-value, implication can be defined by \emph{
 \begin{translation}%
  \trantypej{\typa \Implies \typb}
   {\Not(\typa \And {\Not\typb})} \\
  \tranj{\dualabs{\vara}{\expb}}
   {\comp{\bind{\varc}{\cut{\varc}{\fst{\bind{\vara}{\cut{\varc}{\snd{\cocomp{\expb}}}}}}}}} \\
  \tranj{\dualapp{\expa}{\coexpb}}
   {\cocomp{\pair{\expa}{\comp{\coexpb}}}}.
 \end{translation}%
 } Note translation of a function abstraction is a value.
 \end{proposition}
\end{Slide}


\begin{Slide}{Encoding functions in call-by-name}
\\  \\
\begin{rules}
\dualabsrule \sameline \dualapprule
\end{rules}
\begin{reductions}
  \redjv{\beta\Implies}
   {\cut{\dualabs{\vara}{\expb}}{\dualapp{\expa}{\covalb}}}
   {\cut{\expa}{\bind{\vara}{\cut{\expb}{\covalb}}}} \\
\end{reductions}
\\
 \begin{proposition} Under call-by-name, implication can be defined by \emph{
 \begin{translation}%
  \trantypej{\typa \Implies \typb}
   {{\Not\typa} \Or \typb} \\
  \tranj{\dualabs{\vara}{\expb}}
   {\cobind{\cut{\inl{\comp{\bind{\vara}{\cut{\inr{\expb}}{\covarc}}}}}{\covarc}}{\covarc}} \\
  \tranj{\dualapp{\expa}{\coexpb}}
   {\case{\cocomp{\expa}}{\coexpb}}.
 \end{translation}%
 } The translation of a function application is a covalue.
 \end{proposition}
\end{Slide}


\partslide{Continuation-passing style}


\twice{


\begin{Slide}{Call-by-\pick{value}{name} CPS}
\begin{translation}
  \Trantypej{\Cpstyp{\typx}}
   {\typx} \\
  \reorder{
   \Trantypej{\Cpstyp{\typa \And \typb}}
    {\cpstyp{\typa} \Times \cpstyp{\typb}} \\
  }{
   \Trantypej{\Cpstyp{\typa \Or \typb}}
    {\cpstyp{\typa} \Plus \cpstyp{\typb}} \\
  }
  \Trantypej{\Cpstyp{\Not\typa}}
   {\cpstyp{\typa} \Arrow \typr}
\end{translation}
\end{Slide}


\begin{Slide}{Call-by-\pick{value}{name} CPS}
\small
\begin{translation}
  \Tranj{\Cpsexp{\vara}}
   {\aabs{\covarc}{\covarc\app{\vara}}} \\
  \Tranj{\Cpsexp{\pair{\expa}{\expb}}}
   {\aabs{\covarc}\cpsexp{\expa}\apppar{\aabs{\vara}
                  \cpsexp{\expb}\apppar{\aabs{\varb}
                  \covarc\app{\tpair{\vara}{\varb}}}}} \\
  \Tranj{\Cpsexp{\inl{\expa}}}
   {\aabs{\covarc}{\cpsexp{\expa}\apppar{\aabs{\vara}\covarc\apppar{\tinl{\vara}}}}} \\
  \Tranj{\Cpsexp{\inr{\expb}}}
   {\aabs{\covarc}{\cpsexp{\expb}\apppar{\aabs{\varb}\covarc\apppar{\tinr{\varb}}}}} \\
  \Tranj{\Cpsexp{\comp{\coexpa}}} 
   {\aabs{\covarc}\covarc\app{(\abs{\varc}\cpscoexp{\coexpa}\app{\varc})}} \\
  \Tranj{\Cpsexp{\cobind{\cmda}{\covara}}}
   {\aabs{\covara}{\cpscmd{\cmda}}}  \\[1ex]
  \Tranj{\Cpscoexp{\covara}}
   {\aabs{\varc}\covara\app{\varc}}  \\
  \Tranj{\Cpscoexp{\case{\coexpa}{\coexpb}}}
   {\aabs{\varc}\sumcase{\varc}{\vara}{\cpscoexp{\coexpa}\app{\vara}}{\varb}{\cpscoexp{\coexpb}\app{\varb}}} \\
  \Tranj{\Cpscoexp{\fst{\coexpa}}}
   {\aabs{\varc}\fstcase{\varc}{\vara}{\cpscoexp{\coexpa}\app{\vara}}} \\
  \Tranj{\Cpscoexp{\snd{\coexpb}}}
   {\aabs{\varc}\sndcase{\varc}{\varb}{\cpscoexp{\coexpb}\app{\varb}}} \\
  \Tranj{\Cpscoexp{\cocomp{\expa}}}
   {\aabs{\varc}(\abs{\covarc}\cpsexp{\expa}\app{\covarc})\app{\varc}} \\
  \Tranj{\Cpscoexp{\bind{\vara}{\cmda}}}
   {\aabs{\vara}\cpscmd{\cmda}}  \\[1ex]
  \Tranj{\Cpscmd{\cut{\expa}{\coexpa}}}
   {\cpsexp{\expa}\app{\cpscoexp{\coexpa}}}
\end{translation}
\end{Slide}


\begin{Slide}{CPS preserves types}
\begin{proposition}
The call-by-\pick{value}{name} CPS translation preserves types.
 \[\colored
 \left.
 \ba{r}
 \expj{\enva}{\vala}{\typa}{\coenva} \\
 \reorder{
  \expj{\enva}{\expa}{\typa}{\coenva} \\
 }{
  \coexpj{\enva}{\coexpa}{\typa}{\coenva} \\
 }
 \cmdj{\enva}{\cmda}{\coenva}
 \ea
 \right\}
\IFF
 \left\{
 \ba{l}
 \Expj{\ext{\Cpstyp{\enva}}{\Cpstyp{\Not\coenva}}}{\Cpsval{\vala}}{\Cpstyp{\typa}} \\
 \reorder{
  \Expj{\ext{\Cpstyp{\enva}}{\Cpstyp{\Not\coenva}}}{\Cpsexp{\expa}}{\Cpstyp{\Not\Not\typa}} \\
 }{
  \Expj{\ext{\Cpstyp{\enva}}{\Cpstyp{\Not\coenva}}}{\Cpsexp{\coexpa}}{\Cpstyp{\Not\typa}} \\
 }
 \Expj{\ext{\Cpstyp{\enva}}{\Cpstyp{\Not\coenva}}}{\Cpsexp{\cmda}}{\Tp{\typr}}
 \ea
 \right.
 \]
\end{proposition}
\end{Slide}


\begin{Slide}{CPS preserves and reflect reductions}
\begin{proposition}
Let $\expa$, $\coexpa$, $\cmda$
be in the dual calculus, and $\expb$, $\coexpb$, $\cmdb$ be in the
CPS target calculus.  Then
 \[\colored
 \left.
 \ba{r}
 \reorder{
  \tm{\expa \becomesv \uncpsexp{\expb}} \\
 }{
  \tm{\coexpa \becomesv \uncpscoexp{\coexpb}} \\
 }
 \tm{\cmda \becomesv \uncpscmd{\cmdb}}
 \ea
 \right\}
 \IFF
 \left\{
 \ba{l}
 \reorder{
  \Tm{\cpsexp{\expa} \Becomes \expb} \\
 }{
  \Tm{\cpscoexp{\coexpa} \Becomes \coexpb} \\
 }
 \Tm{\cpscmd{\cmda} \Becomes \cmdb},
 \ea
 \right.
 \mbox{and}~
 \ba{l@{\,}c@{\,}l}
 \reorder{
  \Tm{\Cpsexp{\Uncpsexp{\expb}}} &\Tm{\equiv}& \Tm{\expb} \\
 }{
  \Tm{\Cpscoexp{\Uncpscoexp{\coexpb}}} &\Tm{\equiv}& \Tm{\coexpb} \\
 }
 \Tm{\Cpscmd{\Uncpscmd{\cmdb}}} &\Tm{\equiv}& \Tm{\cmdb}.
 \ea
 \]
\end{proposition}
\end{Slide}


}


\partslide{Conclusions}


\begin{Slide}{Contributions of this work}
\\
\begin{itemize}
\item Replace one connective by three:
\[\colored
\tp{A \Implies B}
\quad \Longrightarrow \quad
\ba{c}
\tp{A \And B} \\ 
\tp{A \Or B} \\ 
\tp{\Not A}.
\ea
\]
\item Encodings:
\[\colored
\ba{rcl@{\quad}l}
\tp{A \Implies B} & \tp{\defeq} & \tp{(\Not A) \Or B}, & \mbox{call-by-name}, \\
\tp{A \Implies B} & \tp{\defeq} & \tp{\Not(A \And (\Not B))}, & \mbox{call-by-value}.
\ea
\]
\item Role of values and covalues clarified.
\item Improved CPS results, following Sabry and Wadler (1997).
\end{itemize}
\end{Slide}


\eat{

\begin{Slide}{Elegance}
\begin{center}
\photo{0.4}{images/pompidou.jpg}{}
\end{center}
Dual calculus less compact than $\lambda$-calculus.  Compare
\[\colored
 \tm{\tfst{\expa}}
\]
with
\[\colored
 \tm{\cobind{\cut{\expa}{\fst{\covara}}}{\covara}}
\]
\end{Slide}


\begin{slide}
\begin{center}\Large
What is the dual of call-by-need?
\end{center}
\end{slide}

}


\begin{Slide}{Implementation}
\\ \\ \\
\begin{center}\large\color{blue}
Implemented by 
Kate Moore, 
Geoffrey Washburn,
Stephanie Weirich,
Steve Zdancewic at U Penn.
\end{center}
\end{Slide}


\begin{Slide}{Another question}
\\ \\ \\
\begin{center}\large\color{blue}
What more will we discover by the
centenary of the birth of $\lambda$-calculus,
natural deduction, and sequent calculus?
\end{center}
\end{Slide}


\end{document}
