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

\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}
\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\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.0cm}}\vss}\strut}
\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{\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{-4em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large functional programming in practice}

\red{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

course `\blue{Principles of Programming Languages}' \\
Free University Amsterdam \\
2006 05 11, 11:00
\end{slide}

\begin{slide}
\sectiontitle{why I use functional languages}
\slidetitle{the story of LCF and ML}
\red{\textbf{proof assistants}} = {programs to help create correct mathematical proofs}
\adviwait
\medskip

\textsl{research on proof assistants} \green{$\longrightarrow$ \red{functional programming}} \\
\adviwait
\phantom{\textsl{research on proof assistants}} \green{$\longrightarrow$ emacs}
\adviwait
\bigskip

\blue{{functional programming} = `spin off' of proof assistant technology}
%\adviwait
\medskip

\vspace{-1.1\bigskipamount}
\vbox to 0pt{
\vspace{.2cm}
\hbox to \hsize{\hfill\includegraphics[height=8em]{/home/freek/talks/fp/milner0.eps}\hspace{-1.3cm}}
\vss
}
\textbf{Robin Milner} {$\longrightarrow$ {Turing award in 1991}}
\vspace{-\smallskipamount}
\begin{itemize}
\item[]

{process algebra} \green{$\longrightarrow$ \small{CCS} $\longrightarrow$ $\pi$-calculus} \\
{proof assistants} \green{$\longrightarrow$ \red{LCF proof assistant}}
\vspace{-.5\smallskipamount}
\begin{itemize}
\item[]
{`Logic of Computable Functions'} \\
\adviwait
\textsl{scripting language for LCF} \green{$\longrightarrow$ \red{ML = `meta language'}}
\end{itemize}
\end{itemize}

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

\begin{slide}
\slidetitle{functional languages}

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

\advirecord{a5}{
prehistoric (1958), big, \textsl{untyped}
}
\medskip

\item[$\bullet$]
\textbf{ML}

\advirecord{a6}{
typed, \textsl{strict}, \green{supports imperative programming}

\advirecord{a9}{
\begin{itemize}
\item[--]
\textbf{SML} = standard ML

\item[\advirecord{a3}{--}\adviplay{a3}]
\advirecord{a1}{\textbf{ocaml}}\adviplay{a1}

\end{itemize}
}
}
\medskip

\item[\advirecord{a4}{$\bullet$}\adviplay{a4}]
\advirecord{a2}{\textbf{haskell}}\adviplay{a2}

\advirecord{a7}{
typed, \textsl{lazy}, \green{{purely functional}}
}
\medskip

\item[$\bullet$]
\textbf{clean}

\advirecord{a8}{
`improved haskell', \blue{made in Nijmegen}
}

\end{itemize}
\adviwait
\adviplay{a5}
\adviwait
\adviplay{a6}
\adviplay{a7}
\adviwait
\adviplay{a9}
\adviwait
\adviplay{a8}
\adviwait
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{some functional programs}
\slidetitle{functional programs that I really use}
\begin{itemize}
\item[$\bullet$]
\textbf{advi}

\green{`active DVI'}

powerpoint-like \red{presentation software} for {\LaTeX} \\
presents a dvi-file with effects
\medskip
\adviwait

\item[$\bullet$]
\textbf{unison}

\red{file synchronisation} software

keeps two file trees identical \\
runs on Unix, Windows \& Mac
\medskip

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the best proof assistants}
\begin{itemize}
\item[$\bullet$]
\textbf{\small HOL}
\begin{itemize}
\item[--]
\strut\rlap{\textbf{\small HOL4}} \advirecord{b3}{\hspace{8em}$\longrightarrow$ SML}
\item[--]
\strut\rlap{\advirecord{b1}{\textbf{{\small HOL L}ight}}\adviplay{b1}} \advirecord{b4}{\hspace{8em}$\longrightarrow$ ocaml}
\item[--]
\strut\rlap{\textbf{{\small P}roof{\small P}ower}} \advirecord{b5}{\hspace{8em}$\longrightarrow$ SML}
\item[--]
\strut\rlap{\textbf{{\small I}sabelle}} \advirecord{b6}{\hspace{8em}$\longrightarrow$ SML}
\end{itemize}
\item[$\bullet$]
\strut\rlap{\advirecord{b2}{\textbf{coq}}\adviplay{b2}} \advirecord{b7}{\hspace{9.4em}$\longrightarrow$ ocaml}
\item[$\bullet$]
\strut\rlap{\textbf{\small PVS}} \advirecord{b8}{\hspace{9.4em}$\longrightarrow$ lisp \& ocaml}
\item[$\bullet$]
\strut\rlap{\textbf{\small ACL2}} \advirecord{b9}{\hspace{9.4em}$\longrightarrow$ lisp}
\item[$\bullet$]
\strut\rlap{\advirecord{b2a}{\textbf{mizar}}\adviplay{b2a}} \advirecord{b7a}{\hspace{9.4em}$\longrightarrow$ pascal}
\end{itemize}
\adviwait
\adviplay[slidegreen]{b3}
\adviplay[slidegreen]{b4}
\adviplay[slidegreen]{b5}
\adviplay[slidegreen]{b6}
\adviplay[slidegreen]{b7}
\adviplay[slidegreen]{b7a}
\adviplay[slidegreen]{b8}
\adviplay[slidegreen]{b9}
%\adviwait
%\adviplay[slidered]{b1}
%\adviplay[slidered]{b2}
%\adviplay[slidered]{b2a}

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof assistants that are programming languages}

a proof assistant that is also a logic programming language
\begin{itemize}
\item[$\bullet$]
\strut\rlap{\advirecord{c1}{\textbf{twelf}}\adviplay{c1}} \advirecord{c2}{\hspace{8em}$\longrightarrow$ SML}
\end{itemize}
\adviwait
\bigskip
proof assistants that want to be functional programming languages
\begin{itemize}
\item[$\bullet$]
\strut\rlap{\textbf{agda}} \advirecord{c3}{\hspace{8em}$\longrightarrow$ haskell}
\item[$\bullet$]
\strut\rlap{\textbf{epigram}} \advirecord{c4}{\hspace{8em}$\longrightarrow$ haskell}
\end{itemize}
\adviwait
\adviplay[slidegreen]{c2}
\adviplay[slidegreen]{c3}
\adviplay[slidegreen]{c4}
\adviwait
\bigskip
\red{dependently typed} functional programming
\medskip

\blue{functional programming languages steadily become more \rlap{\advirecord{c6}{impractical?}}\advirecord{c5}{abstract}\adviplay[slideblue]{c5}} \\
\green{\textbf{lisp} $\longrightarrow$ \textbf{ML} $\longrightarrow$ \textbf{haskell} $\longrightarrow$ \red{coq} / \red{agda} / \red{epigram} / \dots}
\adviwait
\adviplay[white]{c5}
\adviplay[slideblue]{c6}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{John Harrison's theorem provers}
\slidetitle{HOL Light}

\green{LCF $\longrightarrow$ HOL $\longrightarrow$ \red{HOL Light}}
\adviwait
\medskip

\textbf{John Harrison}
\vspace{-1.1\bigskipamount}
\vbox to 0pt{
\vspace{-1.8cm}
\hbox to \hsize{\hfill\includegraphics[height=6em]{/home/freek/talks/dagen/pics/pentium.eps}\hspace{-1.3cm}}
\vss
} \\
\strut--\ verifies floating point hardware for Intel \\
\adviwait
\strut--\ has verified the most theorems in the world
\vspace{-\smallskipamount}\\
\strut\enskip\ {\small\texttt{\gray{\char`\<}\blue{http://www.cs.ru.nl/\char`\~freek/100/}\gray{\char`\>}}} or google for \gray{\fbox{\small\strut \blue{freek 100}}}
\medskip
\adviwait

\green{HOL Light source} \\
44 files = 25k lines = 1{\small M} source
\adviwait
\medskip

\red{in HOL there is no difference between programming and proving!} \\
HOL proof = ML program that returns an object of datatype `\hspace{.9pt}\green{thm}'

\vfill
\end{slide}

\begin{slide}
\slidetitle{the theorem prover from John's book}

\begin{center}
\medskip
\red{Introduction to Logic and Automated Theorem Proving}
\medskip
\end{center}

currently 820 pages \\
to be published by Cambridge University Press
\bigskip
\adviwait

\green{everything explained through code samples} \\
\adviwait
all code samples together $\longrightarrow$ \red{fully functional proof tool}
%\adviwait
\bigskip

{\small\texttt{\char`\<\blue{http://www.cl.cam.ac.uk/users/jrh/atp/}\char`\>}}
\begin{flushright}
\vspace{-\smallskipamount}
or google for \gray{\fbox{\small\strut \blue{theorem proving examples}}}
\end{flushright}
\adviwait
\adviembed{/home/freek/talks/fp/demo}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{so why functional programming?}
\slidetitle{easy data}
\begin{itemize}
\item[$\bullet$]
algebraic datatypes $+$ pattern matching
\medskip

\begin{quote}\small
\advirecord{d1}{\green{\texttt{(* }\textsl{Type for recording history.}\texttt{\ *)}}}
\vspace{-2\medskipamount}
\begin{alltt}\advirecord{d2}{\green{
type history =
   Start of int
 | Mmul of (num * (int list)) * history
 | Add of history * history;;
}}\end{alltt}
\end{quote}
\medskip

\item[$\bullet$]
\advirecord{d3}{garbage collection}\adviplay{d3}

\end{itemize}
\adviwait
\adviplay[slidegreen]{d1}
\adviplay[slidegreen]{d2}
\adviwait
\adviplay[slidered]{d3}

\vfill
\end{slide}

\begin{slide}
\slidetitle{clean code}

functional programming makes it \dots
\medskip
\smallskip

\begin{itemize}
\item[$\bullet$]
{\dots} much more difficult to get a program that even \green{typechecks}
\bigskip
\adviwait

\item[$\bullet$]
\red{{\dots} much more difficult to get a program that has subtle bugs}

\end{itemize}

\vfill
\end{slide}

\end{document}