
%``We may think of Girard's proof as an iceberg. In the top of it, we find what we usually consider the real proof; underwater, the most  of the matter, consisting of all mathematical preliminaries a reader must know in order to understand what is going on.''
% Stefano Berardi, Girard Normalization Proof in LEGO,

% This work actually had a file "A list of assumptions for Girard's theorem" - it is a list of 20 assumptions needed and not proved. They are usually short syntactic or set-theoretical lemmas necessary for the proof; it includes for example substitution lemma; the author remarked that proving all these tedious, and mostly obvious, assumptions might a) might take some time to check and b) does not add that much to the reliability of the proof. In addition, the program extracted from the proof could be, in most cases too slow to be useful.

% As \cite{Altenkirch:TLCA93} remarked,
%
%\begin{quote}
%``I discovered that the core part of the proof (here proving lemmas about CR)
%is fairly straightforward and only requires a good understanding of the paper
%version. However, in completing the proof I observed that in certain places I
%had to invest much more work than expected, e.g. proving lemmas about
%substitution and weakening.''
%\end{quote}

\documentclass[compress,t,13pt,letterpaper]{beamer}
% 17:30

% compress: Show just a single line in the header
% serif   : Use serif font (default: sans serif)
% t       : Begin at to of page (default: centered)


\usetheme{Frankfurt}

\useoutertheme{DSinfolines}
\useinnertheme{circles}

\usepackage{alltt}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{tikz}

\definecolor{dRed}{rgb}{0.65, 0.0, 0.0}
\newcommand{\dRed}[1]{{\color{dRed}#1}}

\definecolor{dGreen}{rgb}{0.133, 0.56, 0.0}
\newcommand{\mygreen}[1]{{\color{dGreen}#1}}


\include{macro}
\setbeamertemplate{navigation symbols}{} % No navigation symbols!

\usepackage{graphicx}

\usepackage{color}
\usepackage{colortbl}
% {0.0,0.25,0.6,0} or 0,0.61,0.87,0}
   \definecolor{orange}{rgb}{0.75,0.5,0.1}
   \definecolor{myblue}{rgb}{1,1,1}
   \definecolor{mydarkblue}{rgb}{0,0.08,0.45}
   \definecolor{myotherblue}{rgb}{0,0.1,0.7}
   \definecolor{myotherblue}{rgb}{0.5,0,0.5}
   \definecolor{dimgrey}{rgb}{0.8,0.8,0.8}

%\usepackage{soul}
%\usepackage{rotating}
%\usepackage{booktabs}

%\newcommand{\noframe}[1]{\frame{#1}}
\newcommand{\noframe}[1]{}
\newcommand{\nomyframe}[2]{}
\newcommand{\myframe}[2]{\frame{\frametitle{#1}#2}}

\newcommand{\high}[1]{{\color{myotherblue}#1}}
\newcommand{\mathem}[1]{{\color{blue}#1}}
\newcommand{\empiri}[1]{{\color{myotherblue}#1}}
\newcommand{\dimg}[1]{{\color{dimgrey}#1}}

\usepackage[cmtip,all]{xy}
\newcommand{\longsquiggly}{\xymatrix{{}\ar@{~>}[r]&{}}}

\makeatletter
\def\@arg{}
\def\arg#1{
  \def\@arg{#1}
  \ifx\@arg\@empty{}
  \else{#1}\fi} %removed the {#1}
\makeatother

\newenvironment{squote}{\begin{quote}\footnotesize\upshape\color{mydarkblue}\ignorespaces}{\end{quote}}

\newcommand{\squotebullet}{\hspace{-8pt}$\bullet$}

\newcommand{\centerquote}[1]{{\centering\footnotesize\color{mydarkblue}#1\par}}

\newcommand{\stepsto}{\longrightarrow}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}

\newcommand{\clos}[2]{#1[#2]}

\usepackage{paralist}
\newcommand{\bc}{\begin{compactitem}}
\newcommand{\ec}{\end{compactitem}}

\usepackage{xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\ie}{i.\,e.\xspace}

\newcommand{\N}{\ensuremath{\mathbb N}}                       % Natural numbers
\newcommand{\Z}{\ensuremath{\mathbb Z}}                       % Integers
\newcommand{\Q}{\ensuremath{\mathbb Q}}                       % Rationals
\newcommand{\R}{\ensuremath{\mathbb R}}                       % Reals

\newcommand{\const}[1]{\textbf{#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Typesetting Deductions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newbox\tempa
\newbox\tempb
\newdimen\tempc
\newbox\tempd

\def\mud#1{\hfil $\displaystyle{#1}$\hfil}
\def\rig#1{\hfil $\displaystyle{#1}$}

\def\inruleanhelp#1#2#3{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
                        \setbox\tempd=\hbox{$\; #3$}%
                        \setbox\tempb=\vbox{\halign{##\cr
        \mud{#1}\cr
        \noalign{\vskip\the\lineskip}%
        \noalign{\hrule height 0pt}%
        \rig{\vbox to 0pt{\vss\hbox to 0pt{\copy\tempd \hss}\vss}}\cr
        \noalign{\hrule}%
        \noalign{\vskip\the\lineskip}%
        \mud{\copy\tempa}\cr}}%
                      \tempc=\wd\tempb
                      \advance\tempc by \wd\tempa
                      \divide\tempc by 2 }

\def\inrulean#1#2#3{{\inruleanhelp{#1}{#2}{#3}%
                     \hbox to \wd\tempa{\hss \box\tempb \hss}}}
\def\inrulebn#1#2#3#4{\inrulean{#1\quad\qquad #2}{#3}{#4}}

\def\ian#1#2#3{{\lineskip 4pt\inrulean{#1}{#2}{#3}}}
\def\ibn#1#2#3#4{{\lineskip 4pt\inrulebn{#1}{#2}{#3}{#4}}}

\def\lowerhalf#1{\hbox{\raise -0.8\baselineskip\hbox{#1}}}

\def\ianc#1#2#3{{\lineskip 4pt\lowerhalf{\inruleanhelp{#1}{#2}{#3}%
                   \box\tempb\hskip\wd\tempd}}}
\def\ibnc#1#2#3#4{{\lineskip 4pt\ianc{#1\quad\qquad #2}{#3}{#4}}}
\def\icnc#1#2#3#4#5{{\lineskip 4pt\ibnc{#1\quad\qquad #2}{#3}{#4}{#5}}}

\def\rulespacing{\renewcommand{\arraystretch}{3} \arraycolsep 5em}
\def\rulestretch{\renewcommand{\arraystretch}{3}}

\def\above#1#2{\begin{array}[b]{c}\relax #1\\ \relax #2\end{array}}
\def\abovec#1#2{\begin{array}{c}\relax #1\\ \relax #2\end{array}}

\def\cian#1#2#3{\ctr{\ianc{#1}{#2}{#3}}}
\def\cibn#1#2#3#4{\ctr{\ibnc{#1}{#2}{#3}{#4}}}

\def\hypo#1#2{\begin{array}[b]{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypoc#1#2{\begin{array}{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypol#1#2#3{\begin{array}[b]{c}\relax #1\\ #2 \\ \relax #3\end{array}}
\def\hypolc#1#2#3{\begin{array}{c}\relax #1\\ #2 \\ \relax #3\end{array}}

\def\ctr#1{\begin{array}{c} #1\end{array}}

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

%---Bibliography

\newcommand{\BGTeubner}{B.\,G.\,Teubner}
\newcommand{\noopsort}[1]{} % Use for explicit references, but not biblogr

\newcommand{\opcit}[1]{\vspace{-8pt}}

\renewcommand{\note}[1]{}
\newcommand{\reprinted}[1]{}
\newcommand{\edition}[1]{}
\newcommand{\comm}[1]{}
\newcommand{\have}[1]{}
\newcommand{\bibseiten}[1]{}
\newcommand{\jfm}[4]{}
\newcommand{\online}[1]{}
\newcommand{\printbibitemlabel}{}
\newcommand{\review}[1]{}
\newcommand{\reviewer}[1]{}
\newcommand{\ppp}[1]{}
\newcommand{\mynote}[1]{}


\newcommand{\beameritemnestingprefix}{a}
% Otherwise error with enumerate environments
% But, numbers don't show!

\usepackage{ifthen}
\usepackage{psfrag}

% -----------------------------------------------------------------------------
\newcommand{\commentsize}{\LARGE} % Default size for comments below slides
                                  % Can be changed by \renewcommand in text
\newcommand{\remark}[1]{{\normalsize [#1]}}
\newcommand{\bifn}[0]{\begin{itemize}\footnotesize}

\newcommand{\amp}{\ \&\ }

\newcommand{\quo}[1]{{\footnotesize ``#1''}}
\renewcommand{\quo}[1]{{\small ``#1''\par}}

% -----------------------------------------------------------------------------

%% Commands used in talk.tex
\newcommand{\punkt}{$\bullet$ }
\newcommand{\ra}{\ensuremath{\rightarrow} }
%\newcommand{\platz}{\item[]}
\newcommand{\platz}{\  \\}
\newcommand{\leer}{({\sc Empty})}
%\newcommand{\commentsize}[1]{}
\newcommand{\topic}[2][empty]{\ifthenelse{\equal{#1}{empty}}%
  {\section{#2}}%then
  {\section{#1 #2}}%else
}
\newcommand{\myfig}[1]{#1}
% \newcommand{\mygreen}[1]{#1}
%\newcommand{\folie}[3]{\begin{slide}{\hspace{9mm}#1\phantom{g}}\sf \vspace{2mm}\leavevmode\hspace{6mm}\begin{minipage}{\textwidth}
\newcommand{\folie}[3]{\myframe{#1}{#2}}
\newcommand{\foliekurz}[3]{\begin{slide}{\hspace{8mm}#1\phantom{g}}\sf \vspace{2mm}
g\small #2\end{slide}}
\newcommand{\keinefolie}[3]{}
%\renewcommand{\labelitemii}{DIRK}
%\renewcommand{\labelitemii}{DIRK}

\newcommand{\darkgoldenrod}{}
\newcommand{\black}{}

\usepackage{amsfonts}
\newcommand{\eu}[1]{\ensuremath{\mathfrak{#1}}}

% -----------------------------------------------------------------------------
\renewcommand{\commentsize}{\large} % Default size for comments below slides
                                    % Can be changed by \renewcommand in text

\newcommand{\tab}{\hspace{16pt}}

\newcommand{\Teil}[1]{\teil{\vspace{-2mm}\\ \hspace{-4mm}#1\dotfill}}

\newcommand{\siehefolie}{\begin{center}\ensuremath{\Box}\end{center}}

\newcommand{\setueber}[1]{\renewcommand{\ueber}{{\darkgoldenrod #1: }}}
\newcommand{\mitte}[1]{\darkgoldenrod\hfill \hspace{-12mm}#1\hfill}

\newcommand{\highlight}{\goldenrod}

\newcommand{\tabbox}[1]{\multicolumn{1}{|c|}{#1}}
%\renewcommand{\tabbox}[1]{\fbox{#1}}

\newcommand{\philsci}{Accounts of scienti{f}ic theories}

\newcommand{\fett}[1]{#1}

% 2005.08.03 Amsterdam Talk

\renewcommand{\setueber}[1]{} % Neutralize previous definitions
\renewcommand{\mitte}[1]{\hfill \hspace{-12mm}#1\hfill}
\newcommand{\ueber}{}

% 2007.10.13 Utrecht Talk

% Note: Replace all "fi" in text by "{f}i" to avoid ligatures that can
%       not be represented by Acrobat Reader.
% Also: Replace "fl" by "{f}l"

\newcommand{\includegraphicscenter}[2]{\begin{center}\includegraphics[#1]{#2}\end{center}}

\newcommand{\cyc}[1]{\ensuremath{\langle #1\/\rangle}}    % cyclic group

\newcommand{\anf}[1]{`#1'}

% Abbreviations:
\newcommand{\dom}{D}
\newcommand{\sys}{S}

% -----------------------------------------------------------------------------

% The following are used by bp

\newcommand{\institution}[1]{}
\newcommand{\darkblue}[1]{#1}

% -----------------------------------------------------------------------------
% -----------------------------------------------------------------------------
% -----------------------------------------------------------------------------

%\documentclass[pdf,bpstyle]{prosper}

\listfiles
% export GS_OPTIONS="-sPAPERSIZE=a4"
% setenv GS_OPTIONS "-sPAPERSIZE=a4"
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{graphicx}
% \usepackage{pstricks,pst-node,pst-tree}
\usepackage{graphics}
\usepackage{psfrag}
\usepackage{color}
\usepackage{code}
\usepackage{proof}
\usepackage{hyperref}
\usepackage{pifont}

\newcommand{\beluga}{\textsc{Beluga}}

% Packages for pretty print contextualML
\usepackage{srcltx}
\usepackage{listings}
\lstloadlanguages{ContextualML}
\lstset{language=ContextualML}  % Added to local lstlang2.sty

\makeatletter
\newtheorem{@theorem}{Theorem}[section]
\renewenvironment{theorem}{\begin{@theorem}\rm}{\end{@theorem}}
\newtheorem{@remark}{Remark}[section]
\newtheorem{@comptyp}{Computation-level Type in Beluga}[section]
\newenvironment{comptyp}{\begin{@comptyp}\rm}{\end{@comptyp}}
\newtheorem{@lfrep}{LF representation in Beluga}[section]
\newtheorem{@lfrepnotitle}{}[section]
\newenvironment{lfrep}{\begin{@lfrep}\rm}{\end{@lfrep}}
\newenvironment{lfrepnotitle}{\begin{@lfrepnotitle}\rm}{\end{@lfrepnotitle}}
\newtheorem{@compcodatatyp}{Computation-level codata types in Beluga using records}[section]
\newenvironment{compcodatatyp}{\begin{@compcodatatyp}\rm}{\end{@compcodatatyp}}
\newtheorem{@compdatatyp}{Computation-level data types in Beluga}[section]
\newenvironment{compdatatyp}{\begin{@compdatatyp}\rm}{\end{@compdatatyp}}
\newtheorem{@comp}{Computation in Beluga}[section]
\newenvironment{comp}{\begin{@comp}\rm}{\end{@comp}}

\makeatother

\newcommand{\mytt}[1]{\lstinline!#1!}
%  \newcommand{\mytt}[1]{\begin{lstlisting} {#1} \end{lstlisting}}

\newcommand{\ttbsl}{\char`\\}

\newcommand{\belann}[1]{{\color{blue}{\texttt{#1}}}}
\newcommand{\belannobj}{\color{blue}{\texttt{on [}} \vdash \texttt{eq (arr A1 A2) (arr B1 B2)]}    }
\newcommand{\emphFact}[1]{{\mygreen{#1}}}
% \newcommand{\emphFact}[1]{{\emph{#1}}}

\renewcommand{\Pi}{\mathchar"7005}
\newcommand{\Pibox}{\Pi^{\scriptscriptstyle\Box}}
\newcommand{\Sigmabox}{\Sigma^{\scriptscriptstyle\Box}}
\newcommand{\entails}{\vdash}
\newcommand{\unifR}{\doteq}

\newcommand{\for}{{/\!\!/}}
\newcommand{\ldot}{.\,}

\newcommand{\vdl}{\vdash^{\!\!\!l}}
\newcommand{\step}{\longrightarrow}


\newcommand{\Psihat}{\hat{\Psi}}
\newcommand{\Gammahat}{\hat{\Gamma}}

\newcommand{\FV}{\m{FV}}
\newcommand{\FMV}{\m{FMV}}
\newcommand{\MV}{\m{MV}}
\newcommand{\V}{\m{V}}

\newcommand{\ev}{\hookrightarrow}
\newcommand{\evv}{\overset{v}{\hookrightarrow}}
\newcommand{\evl}{\overset{l}{\hookrightarrow}}
\newcommand{\conv}{\overset{e}{\rightsquigarrow}} % erase
\newcommand{\convv}{\overset{v}{\rightsquigarrow}} % erase

\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}

% \newcommand{\mdots}{\hspace{-0.085cm}.\hspace{-0.025cm}.\hspace{-0.025cm}.\hspace{-0.025cm}}
\newcommand{\mdots}{}

\newcommand{\nat}{\m{nat}}
% \newcommand{\oftyp}{\;\textsf{oft}\;}
\newcommand{\oftyp}[2]{#1{:}#2}
% \newcommand{\eq}{\;\textsf{eq}\;}
\newcommand{\eq}[2]{#1 = #2}
\newcommand{\syn}{\Rightarrow}
\newcommand{\chk}{\Leftarrow}


\newcommand{\arrow}{\Rightarrow}
\newcommand{\bnfas}{\mathrel{::=}}
\newcommand{\bnfalt}{\mathrel{\mid}}
% \newcommand{\ctxi}[1]{\lceil #1 \rceil}

\newcommand{\proj}{\m{proj}}
\newcommand{\clo}[2]{#1[#2]}
%\newcommand{\boxm}[2]{\m{box}(#1 . \,#2)}
%\newcommand{\boxs}[2]{\m{sbox}(#1.\,#2)}

% \newcommand{\rec}[2]{\m{rec}\;#1 . #2}
\newcommand{\fn}[2]{\m{fn}\;#1 . #2}
\newcommand{\casebox}[2]{\m{case}\;#1\;\m{of}\;#2\;}

% \newcommand{\boxm}[2]{\m{box}(#1.\,#2)}
\newcommand{\boxm}[2]{[#1]\,#2}
\newcommand{\boxp}[2]{\m{pbox}(#1.\,#2)}
\newcommand{\letboxm}[3]{\m{let}\,\m{box}\;#1\;{=}\;#2\;\m{in}\;#3}
\newcommand{\boxs}[2]{\m{sbox}(#1.\,#2)}
\newcommand{\letboxs}[3]{\m{let}\,\m{sbox}\;#1\;{=}\;#2\;\m{in}\;#3}
\newcommand{\casev}[2]{\m{case}\;#1\;\m{of}\;#2}
\newcommand{\caseboxs}[2]{\casev{#1}{#2}}
\newcommand{\casearm}[2]{#1 \mapsto #2}
\newcommand{\rec}[2]{\m{rec}\;#1 . #2}
\newcommand{\mlam}[2]{\lambda^{\scriptscriptstyle\Box} #1.\,#2}
\newcommand{\ctxi}[1]{\lceil #1 \rceil}
\newcommand{\itp}[1]{\lceil #1 \rceil}

\newcommand{\Bnfalt}{\!\!\!\bnfalt}
\def\oftp{\mathord{:}}

\newcommand{\edot}{\cdot}
\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\id}{\m{id}}

\newcommand{\lb}{{[\![}}
\newcommand{\rb}{{]\!]}}
\newcommand{\msub}[1]{\lb #1 \rb}

\newcommand{\expr}{\m{exp}}
\newcommand{\term}{\m{term}}
\newcommand{\lamb}[1]{\m{lam}\;#1}
\newcommand{\clamb}[1]{\m{clam}\;#1}
\newcommand{\lam}[2]{\lambda #1.#2}
% \newcommand{\app}[2]{\m{app}\;#1\;#2}

%
% ---------------------------------------------------------------------------
%
% Set up listings "literate" keyword stuff (for \lstset below)
%
\newdimen\zzlistingsize
\newdimen\zzlistingsizedefault
\zzlistingsizedefault=8pt
% \zzlistingsizedefault=10pt
%\zzlistingsizedefault=11pt
\zzlistingsize=\zzlistingsizedefault
\global\def\InsideComment{0}
\newcommand{\Lstbasicstyle}{\fontsize{\zzlistingsize}{1.05\zzlistingsize}\ttfamily}
\newcommand{\keywordFmt}{\fontsize{1.0\zzlistingsize}{1.0\zzlistingsize}\bf}
\newcommand{\smartkeywordFmt}{\if0\InsideComment\keywordFmt\fi}
\newcommand{\commentFmt}{\def\InsideComment{1}\fontsize{0.95\zzlistingsize}{1.0\zzlistingsize}\rmfamily\slshape}

\newcommand{\LST}{\setlistingsize{\zzlistingsizedefault}}

\newlength{\zzlstwidth}
\newcommand{\setlistingsize}[1]{\zzlistingsize=#1%
\settowidth{\zzlstwidth}{{\Lstbasicstyle~}}}
\setlistingsize{\zzlistingsizedefault}

% The order of the "literate" definitions is significant:
%   later definitions shadow earlier ones.  The \\Pi definition must come
%   *after* the \\ definition, or the first part of \\Pi --- that is, \\ --- will
%   be matched, and instead of $\Pi$ you'll get $\lambda Pi$.
%
\lstset{literate={->}{{$\rightarrow~$}}2 %
                               {=>}{{$\Rightarrow~$}}2 %
                               {|-}{$\vdash$}1 %
                               {id}{{{\smartkeywordFmt id}}}1 % 3 $~$
                               {\\}{{$\lambda$}}1 %
                               {\\Pi}{{$\Pi$}}1 %
                               {\\psi}{{$\psi$}}1 %
                               {\\gamma}{{$\Gamma$}}1 %
                               {FN}{{$\Lambda$}}1 %
                               {block}{\keywordFmt block }1
                               {[]}{{\color{blue}[]}}1 %
                               {<<}{\color{myotherblue}}1 %
                               {<b}{\color{blue}}1 %
                               {<<r}{\color{dRed}}1 %
                               {<*}{\color{dGreen}}1 %
                               {<dim}{\color{orange}}1 %
                               {>>}{\color{black}}0 %
               ,
               columns=[l]fullflexible,
               basewidth=\zzlstwidth,
               basicstyle=\Lstbasicstyle,
               keywordstyle=\keywordFmt,
               identifierstyle=\relax,
%               stringstyle=\relax,
               commentstyle=\commentFmt,
               breaklines=true,
               breakatwhitespace=true,   % doesn't do anything (?!)
               mathescape=true,   % interprets $...$ in listing as math mode
%               tabsize=8,
               texcl=false}

% ---------------------------------------------------------------------------

%\newcommand{\x}{\ensuremath{\lambda}}

%\renewenvironment{lstlisting}{\begin{code}}{\end{code}}

\newcommand{\NOoverlays}[2]{}

% ---------------------------------------------------------------------------


\title[POPLMark Reloaded!]
{\darkblue{POPLMark Reloaded!}}


\author[A. Abel, A. Momigliano, B. Pientka]{Andreas Abel \inst{1} \and Alberto Momigliano \inst{2}
             \and Brigitte Pientka \inst{3}}
\institute[shortinst]{\inst{1} Department of Computer Science and Engineering, Gothenburg University, Sweden \and %
                      \inst{2} DI, Universit\`a degli Studi di Milano, Italy \and
                      \inst{3} School of Computer Science, McGill University, Montreal, Canada
                     }



%\date{\begin{picture}(0.0,0.0)
%  \put(-35,145){\includegraphics[width=25mm]{mcgill-letterhead-logo}}
%  \put(-35,128){\includegraphics[width=25mm]{mcgill-letterhead-logo}}
% \put(+40,10){\includegraphics[width=5cm,clip=true]{small-beluga-75.jpg}}
%\end{picture}

% Joint work with Andrew Cave
% \begin{picture}(10cm,4cm)
%   
% \end{picture}
% 
% Currently at: Ludwig Maximilian University Munich, Germany
% }
% \includegraphics[scale=0.12,clip=true]{small-beluga-75.pdf}

\begin{document}
\sf
\maketitle

% \newcommand{\bbox}{\tiny\colC\ensuremath{\blacksquare}}
\newcommand{\bbox}{--}

\newcommand{\impl}{\supset}
\newcommand{\xmark}{\text{\ding{55}}}
%----------------------------------------------------------------------------

% \section{Introduction}

\begin{frame}\frametitle{POPLMark Reloaded: A new benchmark for mechanizing meta-theory of programming languages}%-------------------------------------------------

\Large
% A new benchmark for mechanizing meta-theory of programming languages:\\
\begin{center}
\begin{tabular}{p{10cm}}
Strong normalization of the simply-typed lambda-calculus using
Kripke-style  %% ? needed?
logical relations.
\end{tabular}
\end{center}


% Rest of the talk:
% = Why do we need a new benchmark?
% = Why this particular benchmark?
% = How do we evaluate success?


\end{frame}

%----------------------------------------------------------------------------
\begin{frame}\frametitle{Question 1}%-------------------------------------------------
\vspace{4em}
\begin{center}
\LARGE\textbf
{Why do we need a (new) benchmark?}
\end{center}
\end{frame}

%----------------------------------------------------------------------------
\begin{frame}\frametitle{Before 2005: A Brief Incomplete History}%-------------------------------------------------
% A brief incomplete history of mechanizing meta-theory
\begin{itemize}
\item Isabelle [1986], Coq[1989], Alf/Agda~1 [1990 -- 2007], Lego [1995/98], Elf/Twelf[1993/1998], $\ldots$
\item Case studies: Type Soundness, Church Rosser, Cut-elimination, Compilation, $\ldots$
\item Focus on reasoning about formal systems by structural induction; modelling variable bindings; assumptions; etc.
\item Canonical example: Type soundness
\item Some normalization proofs:
  \begin{itemize}
  \item Altenkirch, SN for System F in Lego [TLCA 1993]
  \item Barras/Werner, SN for CoC in Coq [1997]
  \item C. Coquand, NbE for $\lambda\sigma$ in ALFA [1999]
  \item Berghofer, WN for STL in Isabelle [TYPES 2004]
  \item Abel, WN/SN for STL in Twelf [LFM 2004]
  \end{itemize}
\end{itemize}


\end{frame}
%----------------------------------------------------------------------------
\begin{frame}\frametitle{POPLMark Challenge: Mechanize System F$_<$ [2005]}%-------------------------------------------------

\begin{itemize}
 \item Spotlight on

 \begin{center}\begin{tabular}{p{10cm}}
 {\small{\emph{``type preservation and soundness, unique decomposition properties of operational semantics, proofs of equivalence between algorithmic and declarative versions of type systems.''}}}
   \end{tabular}
 \end{center}

\item Focus on representing and reasoning about structures with binders
\item Easy to be understood; text book description (TAPL)
\item Small (can be mechanized in a couple of hours or days)
\item Explore more systematically different proof environments
\end{itemize}

\end{frame}

%----------------------------------------------------------------------------
\begin{frame}\frametitle{POPLMark Challenge: Looking  back}%-------------------------------------------------


\begin{itemize}
\item[\checkmark] Popularized the use of proof assistants
\item[\checkmark] Many submitted solutions
\item[\checkmark] Explored different techniques for representing bindings
\item[\checkmark] Good way to learn about a technique / proof assistant\\[1ex]
\vspace{1ex}
\pause
\item[?] Long Term Goal: ``a future where the papers in conferences such as POPL and ICFP are routinely accompanied by mechanically checkable proofs of the theorems they claim.''
\item[?] Better understanding of the theoretical foundations of proof environments
\vspace{1ex}
\pause
\item[\xmark] Inspired the development of new theoretical foundations
\item[\xmark] Better tool support
\end{itemize}

\end{frame}

\begin{frame}
  \frametitle{Beyond the POPLMark Challenge}

  \begin{quote}
``The
POPLMark
Challenge is not meant to be exhaustive: other aspects of programming language theory raise formalization difficulties that are interestingly
different from the problems we have proposed —- to name a few: more complex
binding constructs such as mutually recursive definitions,
\emphFact{logical relations proofs}, coinductive simulation arguments, undecidability results, and linear handling of
type environments.'' [Aydemir et. al. 2005]
  \end{quote}


\end{frame}


% \begin{frame}\frametitle{Orbi: Benchmarks for reasoning with binders }%-------------------------------------------------

% Equivalence of algorithmic and declarative equality on normal lambda-terms

% \begin{itemize}
% \item[\checkmark] Highlighted issues surrounding binders and contexts \\(subsumption, context relations)
% \item[\checkmark] Lead to automated support for contexts in Abella [LFMTP'15?]
% \item[\checkmark] Lead to a deeper understanding of the challenges
%   when reasoning with contexts
% \item[\checkmark] Simple, easy to replicate
% \item[\checkmark] Good base line for testing systems
% \vspace{1.5ex}
% %\pause
% \item[---] Narrow focus; narrow impact
% \end{itemize}

% \end{frame}


\begin{frame}\frametitle{POPLMark Reloaded: Goal}%-------------------------------------------------

Benchmark problems that

\begin{itemize}
\item Push the state of the art in the area and outline new areas of research
\item Compare systems and mechanized proofs qualitatively
\item Understand what infrastructural parts should be generically supported and factored
\item Find bugs in existing proof assistants
% \item Realistic Example
\item Highlight theoretical limitations of existing proof environments
\item Highlight practical limitations of existing proof environments
\end{itemize}

\end{frame}


%----------------------------------------------------------------------------
\begin{frame}\frametitle{Question 2}%-------------------------------------------------
\vspace{4em}
\begin{center}
\LARGE\textbf
{Why pick strong normalization for simply-typed lambda-calculus using
Kripke-style
logical relations?}
\end{center}

\pause
In particular:
\begin{enumerate}
\item We can prove SN without (Kripke-style) logical relations and we've already done it.
% \item
\end{enumerate}

\end{frame}

\begin{frame}\frametitle{Witness 1: Lego [Altenkirch'93]}

$\ldots$ ``following Girard's Proofs and Types''
\\[1em]
Characteristic Features:
  \begin{itemize}
    \item Terms are not well-scoped or well-typed
    \item Candidate relation is untyped and does not enforce
      well-scoped terms
$\Longrightarrow$ does not scale to typed-directed evaluation or equivalence\\
$\Longrightarrow$ maybe better techniques to modularize and structure proof
  \end{itemize}

\end{frame}



\begin{frame}\frametitle{Witness 2: Abella, ATS/HOAS}\relax%-------------------------------------------------
% \pause
$\ldots$ ``following Girard's Proofs and Types''
\pause

\begin{itemize}
% \item Lego [T. Altenkirch'93]: Untyped candidate relation
% - terms are not well-scoped
% - types are are well-scoped
% - Candidate relation is untyped; works on not well-scoped terms;
%   that's why you don't need Kripke-style
%
\item Strictly speaking:% \emph{SN for simply-typed $\lambda$-calculus plus constants.}
\begin{center}
\begin{tabular}{p{10cm}}
\emph{SN for simply-typed $\lambda$-calculus plus one constant.}
\end{tabular}
\end{center}

\item Adding a constant significantly simplifies the proof
\item Reducibility of terms only defined on closed terms
\\[1ex]
\item Strictly speaking:
\begin{center}
\begin{tabular}{p{10cm}}
\emph{Show that SN for simply-typed $\lambda$-calculus plus one
  constant implies also SN for open simply-typed $\lambda$-terms}
\end{tabular}
\end{center}
\end{itemize}

\end{frame}


\begin{frame}
  \frametitle{More Witnesses $\ldots$}

  \begin{itemize}
  \item Berghofer : Program extraction from a proof of weak
    normalization using Isabelle [2004]
\\
$\Longrightarrow$ Uses de Bruijn encoding (not well-scoped or
well-typed)\\
% $\Longrightarrow$ Uses de Bruijn encoding (not well-scoped or well-typed)\\
$\Longrightarrow$ ``Compact'' mechanization (800 lines)
\\[1em]
\pause
\item Berger et al. [TLCA'93]: Extraction of a normalization by
  evaluation using strong evaluation in Minlog\\
$\Longrightarrow$ Uses well-scoped de Bruijn encoding \\% (not
                                % well-scoped or well-typed)
$\Longrightarrow$ Domain theoretic semantics
\\[1em]
\pause
\item Doczkal, Schwinghammer [LFMTP'09]:
Mechanization of Strong Normalization Proof for Moggi’s Computational
Metalanguage in Isabelle/Nominal\\
$\Longrightarrow$ Use of nominals avoids Kripke-style formulation
\end{itemize}
\end{frame}



\begin{frame}{Why Kripke-style?}

  \begin{itemize}
  \item Kripke-style extensions cannot be avoided when we attempt to
    prove properties about type-directed evaluation
\\
{\small{(see for example mechanizations of Crary's proof of
    completenes of algorithmic equality for LF)}}
\\[1em]
  \item We want to keep the benchmark problem simple, but it should
    exhibit features that allow us to scale systems to more complex problems.
  \end{itemize}


\end{frame}



\begin{frame}{Setting the Stage: Simply Typed Lambda-Calculus}
  \begin{small}

\[
\begin{array}{ll@{~\bnfas~}l}
\mbox{Terms} & M, N & x \bnfalt \lam {x{:}T} M \bnfalt M \app N \\
\mbox{Types} & T, S & B \bnfalt T \arrow S\\
%%\mbox{Values} & V & \lam x.M
\mbox{Context} & \Gamma & \cdot\bnfalt\Gamma, x\oftp T\\
\mbox{Subs} & \sigma & \epsilon\bnfalt\sigma, N/x
\end{array}
\]


\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$\Gamma \vdash \tmhastype M
    T$}\quad\mbox{Term $M$ has type $T$ in context $\Gamma$} }
\\[1em]
\infer{\Gamma \vdash \tmhastype x T}{\tmhastype x T \in \Gamma} \quad
\infer{\Gamma \vdash \tmhastype {(\lam {x\oftp T} M)} {(T \arrow S)}}
                 {\Gamma, \tmhastype x T \vdash \tmhastype M S}
 % \\[1em]
\quad
\infer{\Gamma \vdash \tmhastype {(M \app N)} S}
             {\Gamma \vdash \tmhastype M (T \arrow S)
  & \Gamma \vdash \tmhastype N T}
\end{array}
\]

\pause
\vspace{1ex}
\textbf{Implement well-typed lambda-terms any way you like!}\\
Intrinsically typed, explicit typing, explicit typing context,
HOAS-style, Nominal, de Bruijn, $\ldots$

  \end{small}
\end{frame}


\begin{frame}{Setting the Stage: Evaluation}
  \begin{small}

\[
\begin{array}{c}
\multicolumn{1}{l}{\fbox{$\Gamma \vdash M \Steps M'$}~~\mbox{Term $M$ steps to term $M'$ in  context $\Gamma$}}
\\[1em]
\infer{\Gamma \vdash\lam {x\oftp T}M \Steps \lam {x\oftp T} M'}{\Gamma,x\oftp T \vdash M \Steps M'} \qquad
\infer{\Gamma \vdash (\lam {x\oftp T} M) \app N \Steps [N/x]M}{} \\[1em]%\qquad
\infer{\Gamma \vdash M \app N \Steps M'\;N}{\Gamma \vdash M \Steps M'} \quad
\infer{\Gamma \vdash M \app N \Steps M\;N'}{\Gamma \vdash N \Steps N'}
 \\[2em]
% \multicolumn{1}{l}{\fbox{$M \MSteps M'$}~~ \mbox{Term $M$ steps in
%     multiple steps to term $M'$}}\\[1em]
% \infer[\MRef]{M \MSteps M}{} \qquad
% \infer[\MOne]{M \MSteps M'}{M \Steps N & N \MSteps M'}
\end{array}
\]

\vspace{2ex}
\textbf{Remark}: We chose to make $\Gamma$ explicit in the evaluation rules;
  \textbf{this is not a requirement!} -- But your implementation of the
    rules must allow for evaluating terms with free variables.




  \end{small}

\end{frame}


\begin{frame}{Setting the Stage: Reducibility}

  \begin{center}
\textbf{Reducibility must be defined on well-typed open terms!}
  \end{center}
\vspace{1ex}
\pause
% \alt<2>{
\begin{definition}
 [Reducibility Candidates: $\rcs \Gamma M B$]
\mbox{}
\begin{tabular}{l@{~}c@{~}lll}
  $\Gamma \vdash M$ & $\in$ & $B$ & iff & $\Gamma\vdash M\hastype B$
                                          and $\sn \Gamma M$\\
  $\Gamma \vdash M$ & $\in$ & ${T\arrow S}$ & iff &
$ \Gamma\vdash M\hastype {T\arrow S}$ and  \\
  & & & & for all $N,\Delta$ such that
  $\Gamma \leq_\rho \Delta$,  \\
  & & & & ~~~~~~if $\rcs \Delta N {T}$ then
  $\rcs \Delta {([\rho]M) \app N} {S}$.

\end{tabular}
% \begin{itemize}
% \item $\rcs \Gamma M B$ iff $\Gamma\vdash M\hastype B$ and $\sn \Gamma M$
% \item $\rcs \Gamma M {T\arrow S}$ iff
%   $ \Gamma\vdash M\hastype {T\arrow S}$ and for all $N,\Delta$ such that
%   $\Gamma \leq_\rho \Delta$, if $\rcs \Delta N {T}$ then
%   $\rcs \Delta {([\rho]M) \app N} {S}$.
% \end{itemize}
\end{definition}
\vspace{1ex}
\begin{itemize}
\item Contexts arise naturally when we want to state properties about
  well-typed terms and we want to be precise.
\item The definition scales to dependently typed setting and stating
  properties about type-directed equivalence of lambda-terms.
% type directed reductions
\end{itemize}
\pause
\vspace{1ex}
\alt<3>{\centering \textit{Do we really need the weakening substitution
  $\rho$?}}
{\centering \textit {Do we really need to model terms in a ``local'' context and
  use Kripke-style context extensions?}}
\pause
% }{}


\end{frame}




\begin{frame}{Setting the Stage: Strong Normalization}

Often defined as:

\[
\infer[]{\csn \Gamma M}{\forall M'.~\Gamma\vdash M\Steps M' \Longrightarrow \csn \Gamma {M'}}
\]
\vspace{1ex}
\pause
Alternative approach (R. Matthes and F. Joachimski, AML 2003)
  \begin{itemize}
  \item Inductive characterization of normal forms ($\sn \Gamma M$)
  \item Normalization proof is by induction on normal forms and
type expressions
  \item Leads to modular proofs -- on paper and in mechanizations
  \item Show: $\csn \Gamma M$ iff $\sn \Gamma M$.
  \end{itemize}
\end{frame}


\begin{frame}{Why do we think this is an interesting case study?}
  \begin{itemize}
  \item Richer induction principles needed than just structural
    induction based on sub-derivations
  \item Stratified definitions for reducibility candidates
  \item Comparison and trade-offs when modelling well-scoped and
    well-typed terms
  \item Good way to teach logical relations proofs\\
$\Longrightarrow$ maybe extend it to products and sums
  \end{itemize}


\end{frame}


\begin{frame}{A Call for Action}
  \begin{itemize}
  \item Be part of formulating and tackling the challenge
%  \item Help us prepare a tutorial on strong normalization using
%    Kripke-style logical relations
% states clearly the problem, can be read and then implemented more or
% less straightforwardly
  \item Choose your favorite proof assistant and complete the
    challenge
  \item Be part of analyzing mechanizations\\[1em]~~
  \end{itemize}

  \begin{center}
\Large
Last but not least: Propose a different challenge!     
  \end{center}




\end{frame}


\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
