\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\definecolor{slideorange}{rgb}{1,.5,0}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut avoiding state with infinite contexts}

\green{Freek Wiedijk} \\
Radboud University Nijmegen \\
The Netherlands
\medskip

\red{10th Asian Logic Conference} \\
\gray{special session:} model theory and proof theory \\
Kobe, Japan
\medskip

{2008\hspace{3pt}09\hspace{3pt}05, 15\hspace{1pt}:\hspace{1.8pt}40}

\end{slide}

\begin{slide}
\sectiontitle{trusting a proof checker}
\slidetitle{proof checking of mathematics}
\green{\textsl{fully} verified for correctness by a computer:}
\begin{itemize}
\vspace{.6\smallskipamount}
\item[$\bullet$]
\red{G\"odel's first incompleteness theorem}

nqthm (1986), Coq (2003), {\small HOL} Light (2005)

\item[$\bullet$]
\red{Jordan curve theorem}

{\small HOL} Light (2005), Mizar (2005)

\item[$\bullet$]
\red{prime number theorem}

Isabelle (2004), {\small HOL} Light (2008)

\item[$\bullet$]
\red{four color theorem}

Coq (2004)

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the de Bruijn criterion}
all software has bugs$\,$\dots \\
\red{why trust a proof checker?}
\medskip
\adviwait

{{N.G.~de Bruijn}, 1968}:
\begin{quote}
{{\small [$\,$\dots]$\,$}
\green{This is one of the reasons for keeping {\small AUTOMATH} as primitive
as possible.}
\small{[$\,$\dots]}}
\end{quote}
\medskip
\adviwait

\textsl{two approaches:}
\begin{itemize}
\item[$\bullet$]
\red{{small independent checker(s)}} \\
e.g.: {Ivy system} for Otter/Prover9

\smallskip
\adviwait
\item[$\bullet$]

\red{{small proof checking \textbf{kernel} inside the system}} \\
\blue{{{\small LCF} architecture}}
\smallskip

{{Robin Milner}, 1972}

\end{itemize}

\vspace{-14pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{systems and kernels}
\green{source sizes in $10^3$ lines of code}
\vbox to 0pt{
\vspace{-1.2em}
\begin{center}
\begin{tabular}{lllrrr}
&&& $\hspace{8pt}$\green{kernel}{\setbox0=\hbox{.7}\hspace{-\wd0}} & $\enskip\,$\green{system}{\setbox0=\hbox{.7}\hspace{-\wd0}}\phantom{.0} & $\hspace{8pt}$\gray{thms}$\;$\\
\noalign{\color{slidegray}{\hrule}}%
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}$\quad$ &
\red{\advirecord{a1}{{\small HOL} Light}} & \gray{\small ocaml} & \red{\advirecord{a2}{0\rlap{.7}}} & 30\phantom{.0} & \gray{69}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/germany.eps} &
{Isabelle} & \gray{\small sml} & 5 & 160\phantom{.0} & \gray{40}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/denmark.eps} &
{Twelf} & \gray{\small sml} & 6 & 70\phantom{.0} & \gray{---}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps} &
{ProofPower}$\hspace{8pt}$ & \gray{\small sml} & 7 & 90\phantom{.0} & \gray{42}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/france.eps} &
{Coq} & \gray{\small ocaml} & \blue{\advirecord{a3}{14}} & 180\phantom{.0} & \gray{39}\phantom{.0} \\
\noalign{\color{slidegray}{\hrule}}%
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/poland.eps}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/japan.eps} &
{Mizar} & \gray{\small pascal} && \blue{\advirecord{a4}{80}}\phantom{.0} & \gray{45}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps} &
{\small ACL2} & \gray{\small lisp} && 170\phantom{.0} & \gray{12}\phantom{.0} \\
\noalign{\smallskip}
\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps} &
{\small PVS} & \gray{\small lisp} && 280\phantom{.0} & \gray{15}\phantom{.0} \\
\noalign{\color{slidegray}{\hrule}}
\end{tabular}
\end{center}
\vss}
\adviplay{a1}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviwait
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}
\adviwait
\adviplay[slideblue]{a4}
\adviwait
\adviplay[black]{a4}
\adviplay[slideblue]{a3}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proving the kernel correct}
\begin{itemize}
\item[$\bullet$]
\red{Coq in Coq} \\
{Bruno Barras, 1997--1999}
\smallskip

\green{executable Coq model of the Coq logic}
\medskip

\blue{two different systems} (the real system versus the extracted code) \\
extracted code not yet used for serious proof development

\medskip
\adviwait
\item[$\bullet$]
\red{{\small HOL} in {\small HOL}} \\
{John Harrison, 2006}
\smallskip

\green{{\small HOL} model of the actual {\small HOL} Light kernel source}
\medskip

\blue{not yet the full code} (no type polymorphism, no definitions) \\
no \textsl{systematic} relation between {\small HOL} model and executable code

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{kernels and state}
{to make proving a kernel feasible:}
\begin{itemize}
\item[$\bullet$]
code should be as `mathematical' as possible
\adviwait

\item[$\bullet$]
\green{for current technology:} \\
{kernel should be programmed in a \red{purely functional} language}

Lisp, \blue{{\small ML}}, Haskell, \blue{Coq}

\end{itemize}

\adviwait
\medskip\smallskip
\green{current practice:}
\begin{itemize}
\item[$\bullet$]
kernels always have a \textbf{state:}

\blue{\red{definitions} from the formalization that already have been processed}
\adviwait

\item[$\bullet$]
corresponds to a \red{{context}} in the formal treatment of the logic
$$\red{\Gamma} \;\vdash\; M : A$$

\end{itemize}

\vspace{-8pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{undo for {\small HOL}}
\slidetitle{abstract datatypes of the {\small HOL} Light kernel}
\vspace{-1.9em}
\begin{alltt}\small
{type \green{hol_type} = private}
| {Tyvar} of string
\gray{\advirecord{b3}{| \advirecord{b4}{Tyapp}\adviplay{b4} of string * hol_type list}}\adviplay{b3}\medskip
{type \green{term} = private}
| {Var} of string * hol_type
{\advirecord{b1}{| \advirecord{b2}{Const}\adviplay{b2} of string * hol_type}}\adviplay{b1}
| {Comb} of term * term
| {Abs} of term * term\medskip
{type \green{thm} = private}
| {Sequent} of term list * term
\end{alltt}
\adviwait
\vbox to 0pt{
\vspace{-15.35em}
\hfill\parbox{105pt}{\footnotesize
\green{\texttt{\char`\#\ {`pi`;;}}\\\adviwait
\texttt{val it :\ \green{term} = \red{`pi`}}\\
\texttt{\char`\# }}
}%
\bigskip
\adviwait
%\adviplay[slidered]{b1}%
\adviplay[slidered]{b2}%

\hfill
\begingroup
\setlength{\unitlength}{1.5pt}
\small
\begin{picture}(70,80)
%\gray{\put(0,0){\framebox(70,80){}}}%
\thicklines
\red{\put(0,60){\framebox(40,10){}}%
\put(0,60){\makebox(20,10){{Const}}}%
\put(20,60){\line(0,1){10}}%
\put(30,60){\line(0,1){10}}}%
\put(25,65){\red{\circle*{1}}}
\put(35,65){\red{\circle*{1}}}
\thinlines
\put(5,80){\red{\vector(0,-1){10}}}
\adviwait
\put(25,65){\vector(0,-1){12}}
\put(25,65){\red{\circle*{1}}}
\put(15,43){\makebox(20,10){\texttt{"pi"}}}
\adviwait
%\adviplay[slideblue]{b3}%
\adviplay[slideblue]{b4}%
\put(35,65){\blue{\vector(0,-1){25}}}
\put(35,65){\red{\circle*{1}}}
\thicklines
\blue{\put(30,30){\framebox(40,10){}}%
\put(30,30){\makebox(20,10){{Tyapp}}}%
\put(50,30){\line(0,1){10}}%
\put(60,30){\line(0,1){10}}}%
\thinlines
\put(55,35){\blue{\circle*{1}}}
\put(65,35){\blue{\circle*{1}}}
\adviwait
\put(55,35){\vector(0,-1){12}}
\put(55,35){\blue{\circle*{1}}}
\put(42,13){\makebox(20,10){\texttt{"real"}}}
\adviwait
\gray{\put(65,35){\vector(0,-1){25}}}%
\put(65,35){\blue{\circle*{1}}}
\thicklines
\put(60,0){{\makebox(10,10){\texttt{\gray{[]}}}}}
\end{picture}%
\endgroup
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the problem with undoing definitions}
\textsl{hypothetical {\small HOL} Light session:}
\smallskip

\begin{alltt}\small
# \adviwait\green{let X0 = new_definition `X = 0`;;}\adviwait
val ( X0 ) : thm = \advirecord{c7}{|- X = 0}\adviplay{c7}
\blue{\advirecord{c1}{#}}\adviplay{c1} \adviwait\blue{\advirecord{c3}{\advirecord{c2}{undo_definition "X";;}
val it : unit = ()}}\adviplay[slidegreen]{c2}\adviplay{c3}\adviwait
# {}\green{let X1 = \advirecord{c8}{new_definition `X = 1`}\adviplay{c8};;}
val ( X1 ) : thm = |- X = 1
# {\adviwait}\green{TRANS (SYM X0) X1;;}
val it : thm = \red{\advirecord{c4}{|- 0 = 1}}\adviplay{c4}
#
\end{alltt}
\adviwait
\adviplay[slideblue]{c1}
\adviplay[slideblue]{c2}
\adviplay[slideblue]{c3}
\medskip
\blue{\advirecord{c5}{undoing definitions}}\adviplay[slideblue]{c5} can \advirecord{c6}{change the meaning}\adviplay[slidered]{c6} of {existing \texttt{thm}s}\adviplay[slidered]{c7}\adviplay[slidered]{c8} \\
\adviwait
\adviplay[slidered]{c4}%
\adviplay[slideblue]{c5}%
\adviplay[black]{c6}%
\adviplay[black]{c7}%
\adviplay[black]{c8}%
\red{inconsistent\exclspace!}
\adviwait

\textsl{$\Rightarrow$ {\small HOL} Light does not support `\blue{undo}'}

\vspace{-8pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{putting the definitions in the names}
\begin{itemize}
\item[$\bullet$]
\textbf{current {\small HOL} Light} \\
names of constants: \white{\advirecord{e1}{\rlap{string}}}\adviplay[slidegreen]{e1}\adviwait\adviplay[white]{e1}%
pair of a \green{string} and a type

\adviwait
\smallskip
\item[$\bullet$]
\textbf{stateless {\small HOL} Light} \\
names of constants: pair of the \green{traditional name} and \red{the definition}
\medskip
\adviwait

comparing equal definitions by \blue{pointer comparison} is cheap
\adviwait

\end{itemize}
\vbox to 0pt{
\vspace{-.5em}
\begin{center}
\begingroup
\setlength{\unitlength}{1.5pt}
\small
\begin{picture}(135,68)
%\gray{\put(0,-7){\framebox(135,75){}}}%
\thinlines
\put(5,68){{\vector(0,-1){8}}}
\thicklines
{\put(0,50){\framebox(40,10){}}%
\put(0,50){\makebox(20,10){{Const}}}%
\put(20,50){\line(0,1){10}}%
\put(30,50){\line(0,1){10}}}%
\thinlines
\put(25,55){{\vector(0,-1){11}}}
\put(20,35){\makebox(10,10){\green{\texttt{"X"}}}}
\put(35,55){{\vector(0,-1){19}}}
\put(28,26){\makebox(10,10){{\texttt{`:num`}}}}
\put(25,55){{\circle*{1}}}
\put(35,55){{\circle*{1}}}
\adviwait
\thicklines
\red{\put(40.54,50){\framebox(10,10){}}}%
\thinlines
\put(45.5,55){\red{\vector(0,-1){31}}}
\put(45.5,55){\red{\circle*{1}}}
\put(30,10){\makebox(77,15)[l]{\red{\Large\texttt{`X} \texttt{=} \texttt{\white{\advirecord{d1}{0`}}\adviplay[slidered]{d1}}\adviwait\adviplay[white]{d1}\hspace{4.35em}\texttt{`}}}}
\thicklines
\red{{\put(50,12){\framebox(40,10){}}}
\put(50,12){\makebox(20,10){{Const}}}%
\put(70,12){\line(0,1){10}}%
\put(80,12){\line(0,1){10}}%
\blue{\put(90.54,12){\framebox(10,10){}}}%
\thinlines
\put(75,17){{\vector(0,-1){11}}}
\put(70,-3){\makebox(10,10){\green{\texttt{"0"}}}}
\put(85,17){{\vector(0,-1){13}}}
\put(95,17){\blue{\vector(0,-1){15}}}
\put(75,17){{\circle*{1}}}
\put(85,17){{\circle*{1}}}
\put(95,17){\blue{\circle*{1}}}}
\put(93,-7){\makebox(42,10)[l]{\blue{{definition of} \texttt{`O`}}}}
\end{picture}%
\endgroup
\end{center}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{nested kernels}
\begin{center}
\begin{tabular}{ccc}
\textbf{current {\small HOL} Light} && \textbf{\advirecord{e1}{stateless {\small HOL} Light}} \\
\noalign{\medskip\smallskip}
\begin{picture}(120,130)
\thinlines
\gray{\put(0,0){\framebox(120,130){}}%
\put(0,0){\makebox(120,0)[lb]{\strut\ system}}}%
\thicklines
{\put(20,20){\framebox(80,100){}}}%
\green{\put(20,20){\makebox(80,0)[lb]{\strut\ kernel}}}%
\put(60,30){\red{\circle*{3}}}
\put(65,30){\makebox(55,0)[l]{\strut\red{state}}}
\end{picture}%
&$\hspace{1em}$&
\adviwait
\adviplay{e1}%
\begin{picture}(120,130)
\thinlines
\gray{\put(0,0){\framebox(120,130){}}%
\put(0,0){\makebox(120,0)[lb]{\strut\ system}}}%
{\put(20,20){\framebox(80,100){}}}%
\thicklines
{\put(30,40){\framebox(60,70){}}}%
\green{\put(30,40){\makebox(60,0)[lb]{\strut\ kernel}}}%
\put(60,30){\red{\circle*{3}}}
\put(65,30){\makebox(55,0)[l]{\strut\red{state}}}
\end{picture}%
\adviwait
\\
\noalign{\medskip\smallskip}
&& \blue{about 10$\,$\% slower}
\end{tabular}
\end{center}

\vspace{-3pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{type theory without explicit contexts}
\slidetitle{first order logic and contexts}

\def\der#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle{\strut{#1}\over\strut\box0}\rlap{\raise1pt\hbox{$\gray{\scriptstyle\,#3}$}}\hss$}}
\def\leaf#1{\displaystyle{\strut\atop\strut #1}}

\begin{center}
\begin{tabular}{ccc}
\textbf{first order logic} && \textbf{\advirecord{f1}{type theory}} \\
\noalign{\vspace{-\bigskipamount}}
$$
\der{
\der{
\leaf{A \,\vdash P(\red{x})}
}
{A \,\vdash \forall x\, P(x)}{{\forall}I}
}
{\vdash A \to \forall x\, P(x)}{{\to}I}
$$
&$\hspace{2em}$&
$$
\advirecord{f2}{\der{
\der{
\leaf{H : A \,,\, \red{x} : D \vdash \gray{M_1 : {}} P(\red{x})}
}
{H : A \,\vdash \gray{M_2 : {}} \Pi x : D.\, P(x)}{{\lambda}}
}
{\vdash \gray{M_3 : {}} A \to \Pi x : D.\, P(x)}{{\lambda}}}
$$
\\
\noalign{\smallskip}
\adviwait
\green{`sea' of free variables} &&
\adviwait
\adviplay{f1}%
\adviplay{f2}%
\adviwait
\green{`free' variables in the context}
\\
\noalign{\vspace{-0.6\medskipamount}}
\adviwait
$$
\hspace{-5em}
\der{
\der{
\leaf{A \,\vdash_{\red{\{ \red{x} \}}} P(\red{x})}
}
{A \,\vdash_{\red{\{\}}} \forall x\, P(x)}{{\forall}I}
}
{\vdash_{\red{\{\}}} A \to \forall x\, P(x)}{{\to}I}
\hspace{-5em}
$$
\\
\noalign{\vspace{1.1\medskipamount}}
\adviwait
\blue{$\hspace{-5em}
\quad\vdash_{\red{\{\}}} \big(\forall x\, P(x)\big) \to \big(\exists x\, P(x)\big)\mbox{\rlap{\black{\ \large ?}}}
\hspace{-4.8em}$}
\end{tabular}
\end{center}

\vspace{-13pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{merging all contexts into an infinite context}
{category of contexts for a given type theory}
\begin{itemize}
\item[$\bullet$]
\textbf{objects:}
$$\mbox{\blue{$\Gamma$}}$$
$\Gamma$ is a finite or countably infinite context

\item[$\bullet$]
\textbf{morphisms:}
$$\blue{\Gamma \mathrel{\buildrel f\over\longrightarrow} \Gamma'}$$
$f$ is an injection mapping the variables from $\Gamma$ to variables from $\Gamma'$
\end{itemize}

\adviwait
\medskip
\blue{this category has pushouts:} \\
\green{every two contexts can be combined into a bigger context}
\adviwait

\blue{direct limit of all contexts:}
\vspace{-.5\smallskipamount}
$$\qquad\red{\Gamma_{\infty}}$$

\vspace{-20pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the system $\Gamma_{\infty}$}
\blue{$\Gamma_{\infty}$}: system equivalent to the {\small PTS} rules but without explicit contexts \\
\blue{(we reuse the name of the infinite context for the system)}

{{\small PTS} = Pure Type System}
\medskip
\adviwait

we write
$$\phantom{\Gamma_{\infty} \vdash {}} M : A$$
to morally mean
$$\red{\Gamma_{\infty} \vdash {}} M : A\medskip$$
\adviwait
\textbf{$\Gamma_{\infty}$ preterms:}
\def\bar{\mathrel{|}}
$$A ::= s \bar \red{\advirecord{g2}{x_i^{\blue{\advirecord{g5}{A}}}}} \bar \green{\advirecord{g1}{x_i}} \bar AA \bar \lambda \green{\advirecord{g3}{x_i}}{:}A.A \bar \Pi \green{\advirecord{g4}{x_i}}{:}A.A\adviplay{g1}\adviplay{g2}\adviplay{g3}\adviplay{g4}\adviplay{g5}\adviwait\adviplay[slidegreen]{g1}\adviplay[slidered]{g2}\adviplay[slidegreen]{g3}\adviplay[slidegreen]{g4}\adviplay[slidered]{g5}\smallskip$$
{two kind of variables:} \red{free variables $x_i^{\blue{\advirecord{g6}{A}}}\adviplay[slidered]{g6}$} and \green{bound variables $x_i$} \\\adviwait\adviplay[slideblue]{g5}\adviplay[slideblue]{g6}%
superscript \blue{$A$} of \red{$x_i^{\blue{A}}$} may be \textsl{any} preterm

\vspace{-16pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{two of the six $\Gamma_{\infty}$ rules}

\def\der#1#2#3{\setbox0=\hbox{$\strut #2$}%
\hbox to\wd0{$\hss\displaystyle{\strut{#1}\over\strut\box0}\rlap{\raise1pt\hbox{$\gray{\scriptstyle\,#3}$}}\hss$}}
\def\leaf#1{\displaystyle{\strut\atop\strut #1}}

\begin{center}
\begin{tabular}{ccc}
\textbf{{\small PTS} rules} && \textbf{\advirecord{h1}{equivalent $\Gamma_{\infty}$ rules}} \\
\noalign{\vspace{-.5\bigskipamount}}%
$$
\der{\leaf{\Gamma \vdash A : s}}
{\Gamma,\, x_i : A \,\vdash x_i : A}{}
\adviwait
\adviplay{h1}
$$
&$\qquad$&
$$
\der{\leaf{A : s}}
{x_i^A : A}{}
$$ \adviwait\\
$$
\der{\leaf{\Gamma \vdash A : s_1 \quad \Gamma,\, x_i : A \vdash B : s_2}}
{\Gamma \vdash \Pi x_i{:}A. B : s_3}{}\adviwait
$$
&&
$$
\der{\leaf{A : s_1 \quad B : s_2}}
{\Pi \green{\advirecord{h2}{x_i}}{:} A. B[\red{\advirecord{h3}{x_j^A}} := \green{\advirecord{h4}{x_i}}] : s_3}{}\adviplay{h2}\adviplay{h3}\adviplay{h4}\adviwait\adviplay[slidegreen]{h2}\adviplay[slidered]{h3}\adviplay[slidegreen]{h4}
$$
\end{tabular}
\end{center}
\bigskip
\bigskip
binding a variable in $\Gamma_{\infty}$: replace a \red{free variable} by a \green{bound variable}

\vfill
\end{slide}

\begin{slide}
\slidetitle{correspondence theorems}

$$\green{\mbox{derivable {\small PTS} judgment} \quad\longleftrightarrow\quad \mbox{derivable $\Gamma_{\infty}$ judgment}}\hspace{.4em}$$
\bigskip
\adviwait

\blue{from left to right:}

\red{alpha convert} the judgement to separate free from bound variables \\
then: remove the context
\bigskip
\adviwait

\blue{from right to left:}

\red{topological sort} of the free variables in the $\Gamma_{\infty}$ judgement \\
then: put them in that order in the context

\vfill
\end{slide}

\begin{slide}
\sectiontitle{implementing $\Gamma_{\infty}$ for {\small LF}}
\slidetitle{the datatypes of the kernel}
\vspace{-1.9em}
\begingroup
\def\one{\hfill\textsf{\red{\advirecord{i1a}{\normalsize $0 = \lambda,\; 1 = \Pi$}}}}
\def\two{\hfill\textsf{\red{\advirecord{i2a}{\normalsize axioms used}}}}
\begin{alltt}\small
type \green{preterm} =
| Star
| Ref of int
| Var of string * preterm
| Const of string * preterm \red{\advirecord{i2b}{* preterm list}}\adviplay{i2b}\two
| App of preterm * preterm
| Bind of \red{\advirecord{i1b}{int *}}\adviplay{i1b} preterm * preterm\one\medskip
type \green{term} = private
| Box
| In of preterm * term \medskip
type \green{red} = private
| Red of preterm * preterm
\end{alltt}
\endgroup
\adviwait
\adviplay[slidered]{i1b}
\adviplay[slidered]{i1a}
\adviwait
\adviplay[slidered]{i2b}
\adviwait
\adviplay[slidered]{i2a}

\vspace{-6pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{difference of this approach with other kernels}
\blue{most purely functional kernels:}
\begingroup
\small
\begin{eqnarray*}
\green{\texttt{App}} & \hspace{-.6em}\texttt{:}\hspace{-.6em} & \texttt{preterm * preterm -> preterm} \\
\green{\texttt{typecheck}} & \hspace{-.6em}\texttt{:}\hspace{-.6em} & \texttt{\blue{state} -> (\red{preterm} -> term)} \\
\blue{\texttt{extend\char`\_state}} & \hspace{-.6em}\texttt{:}\hspace{-.6em} & \texttt{string * \red{preterm} -> \blue{state} -> \blue{state}}
\end{eqnarray*}
\endgroup

\gray{mutually inconsistent {term}s (from mutually inconsistent states) {possible} \\
internally inconsistent {state} {\textsl{not} possible}}
\medskip
\smallskip
\adviwait

\blue{our approach:} \\
\textsl{function application in {\small LCF} style}
\begingroup
\small
\begin{eqnarray*}
\green{\texttt{app}} & \hspace{-.6em}\texttt{:}\hspace{-.5em} & \texttt{\red{term} * \red{term} -> term\phantom{\ \ \ \ \ \ }}
\end{eqnarray*}
\endgroup
\vspace{-1.25\bigskipamount}

\gray{mutually inconsistent {term}s {\textsl{not} possible}}

\vspace{-3pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{comparing kernel sizes}
\vbox to 0pt{
\begin{center}
\vspace{-.8em}
\begin{tabular}{llrr}
\strut{{\textbf{current {\small HOL} Light}}} 
&& \green{all lines} & \green{content} \\
\noalign{\color{slidegray}{\hrule}}%
kernel & \gray{\texttt{\small fusion.ml$\hspace{1em}$}} & \blue{669} & \red{394}\hspace{0em} \\
\noalign{\bigskip}%\noalign{\color{slidegray}{\hrule}\bigskip}%
\strut{{\textbf{stateless {\small HOL} Light}}$\hspace{1em}$} \\
\noalign{\color{slidegray}{\hrule}}%
kernel & \gray{\texttt{\small core.ml}} & \gray{404} & \red{330}\hspace{0em} \\
state & \gray{\texttt{\small state.ml}} & \gray{95} & 71\hspace{0em} \\
\noalign{\bigskip}%\noalign{\color{slidegray}{\hrule}\bigskip}%
\strut{{\textbf{$\Gamma_{\infty}$ for {\small LF}}}} \\
\noalign{\color{slidegray}{\hrule}}%
kernel & & 214 & \red{166}\hspace{0em} \\
convertibility & & \gray{64} & \gray{49}\hspace{0em} \\
typechecker & & 29 & 25\hspace{0em} %\\
%\noalign{\color{slidegray}{\hrule}}%
\end{tabular}$\enskip$
\end{center}
\vss}

\vspace{-8pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{outlook}
\slidetitle{future work}
\textsl{\red{but does this scale?}}\adviwait
\smallskip

\textbf{experiment:}
\begin{center}
\begin{picture}(100,110)
\thicklines
\gray{\advirecord{j1}{\put(50,34.8){\vector(0,-1){9.8}}}}%
\gray{\advirecord{j2}{\put(50,59.8){\vector(0,-1){9.8}}}}%
\gray{\advirecord{j4}{\put(0,0){\framebox(100,25){}}}}\adviplay{j4}%
\gray{\advirecord{j5}{\put(0,60){\framebox(100,50){}}}}\adviplay{j5}%
\thinlines
\gray{\advirecord{j12}{\put(0,75){\line(1,0){100}}}}\adviplay{j12}%
\white{\advirecord{j11}{\put(0,15){\line(1,0){100}}}}\adviplay{j11}%
\put(100,12.5){\makebox(0,0)[l]{\hspace{.9em}{\gray{\advirecord{j9}{$\Gamma_{\infty}$ for {\small LF}}}\adviplay{j9}}}}
\put(100,85){\makebox(0,0)[l]{\hspace{.9em}{\gray{\advirecord{j8}{{\small HOL} Light}}\adviplay{j8}}}}
\put(100,00){\makebox(0,0)[rb]{\strut\blue{\advirecord{j10}{kernel}}\adviplay[slidegray]{j10}\ }}
\put(100,60){\makebox(0,0)[rb]{\strut\gray{kernel}\ }}
\thicklines
\blue{\advirecord{j3}{\put(5,35){\framebox(90,15){\blue{\advirecord{j6}{{\small LF} context for {\small HOL}}}}}}}%
\blue{\advirecord{j7}{\put(0,0){\framebox(100,15){}}}}
\end{picture}
\medskip
\end{center}

\adviwait
\adviplay[slidegreen]{j1}
\adviplay[slidegreen]{j2}
\adviplay[slidegreen]{j3}
\adviplay{j4}
\adviplay{j5}
\adviplay[slidegreen]{j6}
\adviwait
\red{how much slower than current {\small HOL} Light?} \adviwait
\red{100 times? \adviwait
$\infty$ times?}\toolong
\adviwait
\adviplay[white]{j11}
\adviplay[slidegray]{j12}
\adviplay[slidegray]{j1}
\adviplay[slidegray]{j2}
\adviplay[slideblue]{j3}
\adviplay[slidegray]{j4}
\adviplay[slidegray]{j5}
\adviplay[slideblue]{j6}
\adviplay[slideblue]{j7}
\adviplay[slidegray]{j8}
\adviplay[slidegray]{j9}
\adviplay[slideblue]{j10}

\vspace{-12pt}
\vfill
\end{slide}

\end{document}