\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}{.6,.6,.6}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\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}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\large\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\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{-5em}$}

\def\tto{\to\hspace{-5pt}\!\!\to}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large $\lambda 2$}

\red{logical verification} \\
week 12 \\
2004 12 01

\end{slide}

\begin{slide}
\sectiontitle{overview}
\slidetitle{the course}
\begin{center}
$\hspace{-1em}$\begin{tabular}{rcl}
1st order \textbf{propositional} logic &$\leftrightarrow$& {simple} type theory \\
&& {$\qquad\lambda{\to}$} \\
\noalign{\medskip}
1st order \textbf{predicate} logic &{$\leftrightarrow$}& {type theory with \textbf{dependent types}} \\
&& {$\qquad\lambda P$} \\
\noalign{\medskip}
{\textbf{2nd order} propositional logic} &{$\red{\leftrightarrow}$}& {\textbf{polymorphic} type theory} \\
&& \red{$\qquad\lambda 2$}
\end{tabular}$\hspace{-1em}$
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{activities}
\begin{center}
\begin{tabular}{rcccc}
\noalign{\vspace{-\smallskipamount}}
&& \textbf{logic} && \textbf{type theory} \\
\noalign{\vspace{-\smallskipamount}}
&& natural deduction && {type derivations} \\
\noalign{\bigskip\smallskip}
\textbf{on paper} && \lightgray{\rule{1em}{1em}} && \lightgray{\rule{1em}{1em}} \\
\noalign{\medskip\bigskip}
&& $\red{\downarrow}$ && $\red{\uparrow}$ \\
\noalign{\bigskip\bigskip}
\textbf{in Coq} && \lightgray{\rule{1em}{1em}} &$\red{\rightarrow}$& \lightgray{\rule{1em}{1em}}
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{minimal second order propositional logic}
\slidetitle{formulas}
$$
\begin{array}{l}
\mbox{\green{$a$} \green{$b$} \green{$c$} {\dots}} \\
{A} \mathrel{\red{\to}} {B} \\
\gray{\bot} \\
\gray{\top} \\
\gray{\neg {A}} \\
\gray{{A} \land {B}} \\
\gray{{A} \lor {B}} \\
\red{\forall}\hspace{.2pt}\green{a}.\, {A} \\
\gray{{\exists\hspace{.9pt}{a}.}\, {A}}
\end{array}
%\hspace{20em}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\to$}
$$
{
\begin{array}{c}
[A^x] \\
\vdots \\
B
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
\green{I[x]{\to}}
\leqno{\mbox{\rlap{{$\to$ introduction}}}}
$$

$$
{
\begin{array}{c}
\vdots \\
\red{A \to B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
A
\end{array}
\over
\strut
B
}
\enskip
\green{E{\to}}
\leqno{\mbox{\rlap{{$\to$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules for $\forall$}
$$
{
\begin{array}{c}
\vdots \\
B
\end{array}
\over
\strut
\red{\forall a.\, B}
}
\enskip
\green{I\forall}
\leqno{\mbox{\rlap{{$\forall$ introduction}}}}
$$
\vspace{-\smallskipamount}

\blue{\textbf{variable condition:}\quad $a$ not a free variable in any open assumption}
\vspace{-\smallskipamount}

$$
{
\begin{array}{c}
\vdots \\
\red{\forall a.\, B}
\end{array}
\over
\strut
B[a:=A]
}
\enskip
\green{E\forall}
\leqno{\mbox{\rlap{{$\forall$ elimination}}}}
$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{$\lambda 2$}
\slidetitle{terms}
\begin{center}
\begin{tabular}{c}
\red{${*}$, ${\Box}$} \\
$x$, $y$, $z$, {\dots} \\
$M N$ \\
${\lambda}\hspace{.2pt}x {{} : M}{.}\, N$ \\
\red{${\Pi}\hspace{.3pt}x {{} : M}{.}\, N$}
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules}
$$
{
\over
\strut
\vdash
\red{*} : \Box
}
\rlap{\enskip\gray{axiom}}
$$

$$
{
\strut
\Gamma \,\vdash\, M : {\Pi x : A.\, B}
\qquad
\Gamma \,\vdash\, N : A
\over
\strut
\Gamma \,\vdash\, \red{M N} : {B}{{[x := N]}}}
\rlap{\enskip\gray{application}}
$$

$$
{
\strut
\Gamma,\, x : A \,\vdash\, M : B
\qquad
\Gamma \,\vdash\, {\Pi x : A.\, B} : {s}
\over
\strut
\Gamma \,\vdash\, \red{\lambda x : A.\, M} : {\Pi x : A.\, B}
}
\rlap{\enskip\gray{abstraction}}
$$

$$
{
\strut
\Gamma \,\vdash\, A : \blue{s}
\qquad
\Gamma,\, {x : A} \,\vdash\, B : \blue{*}
\over
\strut
\Gamma \,\vdash\, \red{\Pi x : A.\, B} : \blue{*}
}
\rlap{\enskip\gray{product}}
\vspace{-10pt}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules (continued)}
$$
{
\strut
\Gamma \,\vdash\, A : B
\qquad
\Gamma \,\vdash\, C : {s}
\over
\strut
\Gamma,\, \red{x : C} \,\vdash\, A : B
}
\rlap{\enskip\gray{weakening}}
$$

$$
{
\strut
\Gamma
\vdash
A : {s}
\over
\strut
\Gamma,\, x : A\,\vdash\, \red{x} : A
}
\rlap{\enskip\gray{variable}}
$$
\vspace{0pt}

$$
{
\strut
\Gamma \,\vdash\, A : \red{B}
\qquad
\Gamma \,\vdash\, B' : s
\over
\strut
\Gamma \,\vdash\, A : \red{B'}
}
\rlap{\enskip\gray{conversion}}
$$
\rightline{with $\red{B =_\beta B'}$}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the three product rules}
\green{\textbf{all systems}}
$$
{
\strut
\Gamma \,\vdash\, A : \red{*}
\qquad
\Gamma,\, {x : A} \,\vdash\, B : \red{*}
\over
\strut
\Gamma \,\vdash\, {\Pi x : A.\, B} : \red{*}
}
$$

\green{\textbf{only in} $\lambda P$}
$$
{
\strut
\Gamma \,\vdash\, A : \red{*}
\qquad
\Gamma,\, {x : A} \,\vdash\, B : \red{\Box}
\over
\strut
\Gamma \,\vdash\, {\Pi x : A.\, B} : \red{\Box}
}
$$
$$\green{\texttt{nat} \to *}$$

\green{\textbf{only in} $\lambda 2$}
$$
{
\strut
\Gamma \,\vdash\, A : \red{\Box}
\qquad
\Gamma,\, {x : A} \,\vdash\, B : \red{*}
\over
\strut
\Gamma \,\vdash\, {\Pi x : A.\, B} : \red{*}
}
$$
$$\green{\Pi a : *.\, a \to a}$$

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

\begin{slide}
\sectiontitle{Curry-Howard-de Bruijn}
\slidetitle{$\to$ introduction versus abstraction rule}
$$
{
\begin{array}{c}
[\green{A}^x] \\
\blue{\vdots} \\
\green{B}
\end{array}
\over
\strut
\red{A \to B}
}
\rlap{\enskip ${I[{x}]{\to}}$}
\bigskip
$$

$$
{
\strut
\Gamma,\, x : \green{A} \,\vdash\, \blue{M} : \green{B}
\qquad
\gray{\Gamma \,\vdash\, {\Pi x : A.\, B} : {*}}
\over
\strut
\Gamma \,\vdash\, \blue{\lambda x : A.\, M} : \red{\Pi x : A.\, B}
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\to$ elimination versus application rule}
$$
{
\begin{array}{c}
\blue{\vdots} \\
\green{A \to B}
\end{array}
\qquad
\begin{array}{c}
\blue{\vdots} \\
\green{A}
\end{array}
\over
\strut
\red{B}
}
\rlap{\enskip ${E{\to}}$}
\bigskip
$$

$$
{
\strut
\Gamma \,\vdash\, \blue{M} : \green{\Pi x : A.\, B}
\qquad
\Gamma \,\vdash\, \blue{N} : \green{A}
\over
\strut
\Gamma \,\vdash\, \blue{M N} : \red{{B}{{[x := N]}}}
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\forall$ introduction versus abstraction rule}
$$
{
\begin{array}{c}
\blue{\vdots} \\
\green{B}
\end{array}
\over
\strut
\red{\forall a.\, B}
}
\rlap{\enskip $I\forall$}
\bigskip
$$

$$
{
\strut
\Gamma,\, a : {*} \,\vdash\, \blue{M} : \green{B}
\qquad
\gray{\Gamma \,\vdash\, {\Pi a : *.\, B} : {*}}
\over
\strut
\Gamma \,\vdash\, \blue{\lambda a : *.\, M} : \red{\Pi a : *.\, B}
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{$\forall$ elimination versus application rule}
$$
{
\begin{array}{c}
\blue{\vdots} \\
\green{\forall a.\, B}
\end{array}
\over
\strut
\red{B[a:=A]}
}
\rlap{\enskip $E\forall$}
\bigskip
$$

$$
{
\strut
\Gamma \,\vdash\, \blue{M} : \green{\Pi a : *.\, B}
\qquad
\Gamma \,\vdash\, \blue{A} : {*}
\over
\strut
\Gamma \,\vdash\, \blue{M A} : \red{{B}{{[a := A]}}}
}
$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{examples}
\slidetitle{example 1}

$$\red{(\forall b.\, b) \to a}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 2}

$$\red{a \to \forall b.\, (b \to a)}$$
\bigskip
\adviwait

$$
\green{a : * \vdash \Pi b : * .\, (b \to a) : *}\adviwait
$$

corresponds to
$$
\green{
\textstyle \prod_{b \in {\sf Set}} {\cal P}(b)
\in
\mbox{Set}
}
$$

week 10 \blue{$\to$ paradox}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 3}

$$\red{a \to \forall b.\, ((a \to b) \to b)}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{detours and reduction}
\slidetitle{detour elimination for $\to$}
$$
\begin{array}{c}
\displaystyle
{
\displaystyle
{
\begin{array}{c}
\red{[A^x]} \\
\green{\vdots} \\
\green{B}
\end{array}
\over
\strut
A \to B
}
\enskip
I[x]{\to}
\qquad
\red{
\begin{array}{c}
\red{\vdots} \\
A
\end{array}
}
\over
\strut
\green{B}
}
\enskip
E{\to}
\end{array}
\qquad
\adviwait
\mbox{\Large \gray{$\longrightarrow$}}
\qquad\quad
\begin{array}{c}
\red{\vdots} \\
\red{A} \\
\green{\vdots} \\
\green{B}
\end{array}
\bigskip
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{detour elimination for $\forall$}
$$
\begin{array}{c}
\displaystyle
{
{
\displaystyle
{
\begin{array}{c}
\red{\vdots} \\
\red{B}
\end{array}
\over
\strut
\forall a.\, B
}
\enskip
I\forall
}
\over
\strut
\green{B[a:=A]}
}
\enskip
E\forall
\end{array}
\qquad
\adviwait
\mbox{\Large $\gray{\longrightarrow}$}
\qquad\quad
\begin{array}{c}
\red{\vdots}\rlap{$\;^{\textstyle\green{*}}$} \\
\red{B[a:=A]}
\end{array}
\medskip
$$
\hspace{16em}\green{${}^{\textstyle{*}}$ replace $a$ everywhere by $A$}
\bigskip

\vfill
\end{slide}

\begin{slide}
\slidetitle{typing the proof term of a detour}
$$
{
{
\displaystyle
\strut
\begin{array}{c}
\vdots \\
\Gamma,\, x : \red{A} \,\vdash\, \green{M} : \red{B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
\Gamma \,\vdash\, \green{\Pi x : A.\, B} : {s}
\end{array}
\over
\displaystyle
\strut
\Gamma \,\vdash\, \green{\lambda x : A.\,M} : {\Pi x : A.\, B}
}
\qquad
\begin{array}{c}
\vdots \\
\Gamma \,\vdash\, \green{N} : \red{A}
\end{array}
\over
\strut
\Gamma \,\vdash\, \green{{(\lambda x : A.\,M)} N} : \blue{\red{B}{{[x := N]}}}
}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{problems}
\slidetitle{type checking problem}
\begin{itemize}
\item[]
\textbf{input}
\begin{itemize}
\item[]
context \green{$\Gamma$} and
terms \green{$M$} and \green{$N$}
\medskip
\end{itemize}
$$
\red{\Gamma \stackrel{?}{\vdash} M : N}
$$

\item[]
\textbf{output}
\begin{itemize}
\smallskip
\item[]
\strut\rlap{\green{true}}\phantom{false}\quad
\blue{typing judgment is derivable}

\item[]
\green{false}\quad
\blue{typing judgment is not derivable}
\end{itemize}
\bigskip

\item[]
\textsl{generally decidable}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{type synthesis problem}
\begin{itemize}
\item[]
\textbf{input}
\begin{itemize}
\item[]
context \green{$\Gamma$} and
term \green{$M$}
\medskip
\end{itemize}
$$
\red{\Gamma \vdash M : {?}}
$$

\item[]
\textbf{output}
\begin{itemize}
\smallskip
\item[]
\green{true} + term \green{$N$}\\
\strut\phantom{false\quad}%
\blue{typing judgment is derivable with $N$ substituted for $?$}

\item[]
\green{false}\quad
\blue{for no term substituted for $?$ is the judgment derivable}
\end{itemize}
\bigskip

\item[]
\textsl{generally decidable}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{type inhabitation problem}
\begin{itemize}
\item[]
\textbf{input}
\begin{itemize}
\item[]
context \green{$\Gamma$} and
term \green{$N$}
\medskip
\end{itemize}
$$
\red{\Gamma \vdash {?} : N}
$$

\item[]
\textbf{output}
\begin{itemize}
\smallskip
\item[]
\green{true} + term \green{$M$}\\
\strut\phantom{false\quad}%
\blue{typing judgment is derivable with $M$ substituted for $?$}

\item[]
\green{false}\quad
\blue{for no term substituted for $?$ is the judgment derivable}
\end{itemize}
\bigskip

\item[]
\textsl{generally undecidable}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof checking problem}
\begin{itemize}
\item[]
\textbf{input}
\begin{itemize}
\item[]
formula \green{$A$} + {possibly incorrect \green{`proof'}}
\medskip
\end{itemize}
$$\red{\mbox{correct?}}$$

\item[]
\textbf{output}
\begin{itemize}
\smallskip
\item[]
\strut\rlap{\green{true}}\phantom{false}\quad
\blue{the `proof' is a correct proof of $A$}

\item[]
\green{false}\quad
\blue{the `proof' is not a correct proof of $A$}
\end{itemize}
\bigskip

\item[]
\textsl{generally decidable} \\
\textsl{corresponds to type checking problem}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{provability problem}
\begin{itemize}
\item[]
\textbf{input}
\begin{itemize}
\item[]
formula \green{$A$}
\medskip
\end{itemize}
$$\red{A\rlap{?}}$$

\item[]
\textbf{output}
\begin{itemize}
\smallskip
\item[]
\green{true} + \green{proof} of $A$ \\
\strut\phantom{false\quad}%
\blue{$A$ is proved by the proof in the output}

\item[]
\green{false}\quad
\blue{$A$ is not provable}
\end{itemize}
\bigskip

\item[]
\textsl{generally undecidable} \\
\textsl{corresponds to type inhabitation problem}


\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{other notions}
\slidetitle{uniqueness of types}

$$
\left.
\begin{array}{l}
{\Gamma \vdash A : \red{B}} \\
\noalign{\medskip}
{\Gamma \vdash A : \red{B'}}
\end{array}
\enskip
\right\}
\Rightarrow\quad
\green{\red{B} =_{\beta} \red{B'}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{subject reduction}

$$
\left.
\begin{array}{c}
{\Gamma \vdash A : \red{B}} \\
\noalign{\medskip}
\green{\red{B} \tto_{\beta} \red{B'}}
\end{array}
\enskip
\right\}
\Rightarrow\quad
{\Gamma \vdash A : \red{B'}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{Curry-Howard-de Bruijn isomorphism}
\begin{center}
{\red{isomorphism} \\
between \\
the set of \green{proofs} in a logic \\
and \\
the set of \green{typed lambda terms} in a \rlap{type theory}\phantom{logic}}
\end{center}
\bigskip

\begingroup
\large
\begin{itemize}
\item[]
\blue{formulas as types}
\item[]
\blue{proofs as terms}
\end{itemize}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{Brouwer-Heyting-Kolmogorov interpretation}

\begin{center}
\red{intuitive semantics of intuitionistic logic}
\medskip

explains \\
what it means to \green{prove a formula} \\
in terms of \\
what it means to \green{prove its components}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{minimal versus intuitionistic versus classical logic}

\begin{itemize}
\item[$\bullet$]
\textbf{minimal logic}

\green{only \red{$\to$} and \red{$\forall$}}

\item[$\bullet$]
\textbf{intuitionistic logic}

\green{all connectives, just the \red{intro} and \red{elim} rules}

\item[$\bullet$]
\textbf{classical logic}

\green{{\dots} + one of the classical principles}

\strut\quad\red{excluded middle}
$$A \lor \neg A$$
$$\forall a.\, a \lor \neg a$$

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Coq versus the other proof assistants}
\slidetitle{seven provers for mathematics}
\vspace{-2\bigskipamount}

\begingroup
\small
$$\hspace{-8.5em}\xymatrix@R=2.1em{
\txt{\textbf{Mizar}}\ar@(dr,ul)[rrrd]\ar@{.}[rrrr] &&&& \txt{\rlap{\green{\textsl{most mathematical}}}} \\
\txt{\gray{LCF}}\ar[rr]\ar[rrd]\ar@/_1.8pc/[rrrdd] && \txt{\textbf{HOL}}\ar[r] & \txt{\textbf{Isabelle}}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most pure}}}} \\
\txt{\gray{Automath}}\ar[rr] && \txt{$\,$\rlap{\textbf{\red{Coq}}}\phantom{\textbf{NuPRL}} \\\noalign{\smallskip}\textbf{NuPRL}$\!$}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most logical}}}} \\
&&& \txt{\textbf{PVS}}\ar@{.}[r] & \txt{\rlap{\green{\textsl{most popular}}}} \\
\txt{\gray{nqthm}}\ar[rr]\ar@/^.5pc/[rrru] && \txt{\textbf{ACL2}}\ar@{.}[rr] && \txt{\rlap{\green{\textsl{most computational}}}} \\
}
$$
\endgroup

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

\begin{slide}
\slidetitle{foundations}
\begin{itemize}
\item[$\bullet$]
\textbf{primitive recursive arithmetic}

ACL2

\item[$\bullet$]
\textbf{type theory}

\green{typed lambda calculus + inductive types, constructive}

\red{Coq}, NuPRL

\item[$\bullet$]
\textbf{higher order logic}

\green{typed lambda calculus + choice operator, classical}

HOL, Isabelle, PVS

\item[$\bullet$]
\textbf{set theory}

Mizar

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural versus declarative}
\vspace{-\medskipamount}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\green{
\begin{picture}(5,5)
\advirecord{e0}{
\put(0,5){\line(1,0){5}}
\put(.5,4.5){\makebox(0,0){\black{\scriptsize $0$}}}
\put(0,4){\line(1,0){3}}
\put(1,3){\line(1,0){2}}
\put(2,2){\line(1,0){1}}
\put(4,2){\line(1,0){1}}
\put(3,1){\line(1,0){2}}
\put(4.5,.5){\makebox(0,0){\black{\scriptsize $\infty$}}}
\put(0,0){\line(1,0){5}}
\put(0,0){\line(0,1){5}}
\put(1,1){\line(0,1){2}}
\put(2,0){\line(0,1){1}}
\put(3,1){\line(0,1){2}}
\put(4,2){\line(0,1){2}}
\put(5,0){\line(0,1){5}}
}
\adviplay[slidegreen]{e0}
\put(0.2,4.5){\makebox(0,0){\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,4.5){\makebox(0,0){\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,4.5){\makebox(0,0){\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,4.5){\makebox(0,0){\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,3.5){\makebox(0,0){\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,3.5){\makebox(0,0){\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,3.5){\makebox(0,0){\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,3.5){\makebox(0,0){\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,2.5){\makebox(0,0){\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,1.5){\makebox(0,0){\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}
\put(0.2,0.5){\makebox(0,0){\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,0.5){\makebox(0,0){\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}
\put(1.2,1.5){\makebox(0,0){\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,1.5){\makebox(0,0){\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}
\put(2.2,0.5){\makebox(0,0){\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}
\put(3.2,0.5){\makebox(0,0){\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}
\put(4.2,0.5){\makebox(0,0){\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}
\end{picture}
}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%

\begin{itemize}
\item[$\bullet$]
\textbf{procedural}

\begingroup
\small
\green{%
\adviwait
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
E
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
E
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
S
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
E
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
N
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
E
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
S
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
S
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
S
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
W
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
W
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
W
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
S
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
E
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
E
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
E
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidegreen]{e0}
}
\endgroup

HOL, PVS, \red{Coq}, NuPRL

\adviwait
\item[$\bullet$]
\textbf{declarative}

\begingroup
\scriptsize
\green{
\adviwait
(0,0)
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
(1,0)
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
(2,0)
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
(3,0)
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
(3,1)
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
(2,1)
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
(1,1)
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
(0,1)
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
(0,2)
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
(0,3)
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
(0,4)
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
(1,4)
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
(1,3)
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
(2,3)
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
(2,4)
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
(3,4)
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
(4,4)
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%
}\toolong
\endgroup

Mizar, Isabelle

\end{itemize}

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

\end{document}