ADDED presentation/arend-presentation.pdf Index: presentation/arend-presentation.pdf ================================================================== --- presentation/arend-presentation.pdf +++ presentation/arend-presentation.pdf cannot compute difference between binary files Index: presentation/arend-presentation.tex ================================================================== --- presentation/arend-presentation.tex +++ presentation/arend-presentation.tex @@ -13,11 +13,11 @@ \usecolortheme{beaver} \useinnertheme{circles} - \setbeamercovered{transparent} + \setbeamercovered{invisible} % or whatever (possibly just delete it) } @@ -29,19 +29,19 @@ \usepackage[english]{babel} % Make math look a little better \usepackage{eulervm} -% Use Gill Sans for most text +% Use Raleway for most text \usepackage{fontspec} \defaultfontfeatures{Mapping=tex-text} -\setsansfont{Gill Sans MT} +\setsansfont{Raleway} -\title{Arend} +\title{Arend --- Proof Assistant Assisted Pegagogy} \subtitle{A graphical proof assistant for undergraduate computer science education} \author{Andrew V. Clifton} @@ -62,13 +62,113 @@ \begin{frame} \titlepage \end{frame} -\section{Introduction} +\section{Background} + + +\begin{frame}\frametitle{Formal proofs} + +Formal proofs --- an important component of computer science education. + +Prove +\begin{itemize} +\item $\forall x,y \in \mathbb{N}: x + y = y + x$. +\item If $T$ is a complete binary tree with $n = |T|$ nodes, then the height of + any node is at most $\lfloor \log_2 n \rfloor$. +\item The reverse of a regular language $L^\text{r}$ is itself regular. +\end{itemize} + +\end{frame} + + +\begin{frame}\frametitle{Paper proofs} + +Paper proofs are common, but problematic: +\begin{itemize} +\item Too flexible; allow a wide variety of almost correct'' answers. +\item Delayed results; turn in a proof assignment, get results back a week + later. \pause \alert{Batch processing for proofs.} +\item \pause Non-interactive. +\end{itemize} + +\end{frame} + + +\begin{frame}\frametitle{Computer-assisted logic} + +Using computers to do logic is not a new idea: +\begin{itemize} +\item \pause Automated theorem provers (e.g., AUTOMATH) +\item \pause Model checkers +\item \pause \alert{Proof assistants} (Abella, Coq, Arend, etc.) +\end{itemize} + +\end{frame} + + +\begin{frame}\frametitle{Proof assistants} + +A proof assistant +\begin{itemize} +\item \pause \alert{Assists} the user in constructing a \alert{valid} proof. +\item \pause \alert{Forbids} the construction of \alert{invalid} proofs. +\item \pause Presents proofs, complete or not, to the user in a comprehensible + format. +\end{itemize} + +\end{frame} + +\begin{frame}\frametitle{Proof assistants, cont.} + +Some well-known proof assistants: +\begin{itemize} +\item Twelf (previously used in CSCI 217) +\item Coq +\item Abella (currently used in CSCI 217) +\item Agda +\end{itemize} + +\end{frame} + + +\begin{frame}\frametitle{Aside: the Curry-Howard Isomorphism} + +An aside: + +Some proof assistants bridge the gap between functional programming and proofs, +thanks to the \alert{Curry-Howard isomorphism}. + +\begin{definition} +The Curry-Howard isomorphism states that \emph{proofs} are to \emph{propositions} +as \emph{programs} are to \emph{types}. +\end{definition} + +$a : A$ can mean $a$ is a program with type $A$'', or $a$ is a proof of the +proposition $A$''. + +\end{frame} + +\begin{frame}\frametitle{Curry-Howard isomorphism, cont.} + +Some examples: +\begin{itemize} +\item If $p : P$ and $q : Q$ then the pair $(p,q) : P \land Q$. +\item If $p : P$ and $q : Q$ then either $\mathsf{left}(p) : P \lor Q$ or + $\mathsf{right}(q) : P \lor Q$. +\item The most interesting: $P -> Q$ means $P$ implies $Q$''. \pause But it + is also the type of \alert{functions} from $P$ to $Q$. A proof of + $P -> Q$ is a \emph{program} that converts a proof (value) of $P$ into a + proof (value) of $Q$! +\end{itemize} + +(End of aside.) + +\end{frame} -\subsection{Demostration} + \begin{frame} \vfill \centering