\usepackage{amssymb}
\usepackage[inference, shorthand]{semantic} % Inference rules, shortcuts

% ???
\usepackage[english]{babel}

% Make math look a little better


\usepackage{eulervm}

% Use Raleway for most text
\usepackage{fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setsansfont{Raleway}

................................................................................

\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}

................................................................................
\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.
................................................................................
\end{itemize}

(End of aside.)

\end{frame}















































\begin{frame}
\vfill
\centering
A quick demo of a proof in Arend
\vfill










































































































































































































































































































































































































































\end{frame}


%%% --------------------------------------------------------------------------
%%% Bibliography slide
%%% --------------------------------------------------------------------------

................................................................................
\section<presentation>*{\appendixname}
\subsection<presentation>*{For Further Reading}

\begin{frame}{For Further Reading}
    
  \begin{thebibliography}{10}
    
  \beamertemplatebookbibitems
  % Start with overview books.


  \bibitem{Hillis:1989:CM:64121}
    W.~Daniel~Hillis
    \newblock {\em The Connection Machine}.
    \newblock MIT Press, 1989.
 
    
  \beamertemplatearticlebibitems
  % Followed by interesting articles. Keep the list short. 




  \bibitem{Hillis:1986:DPA:7902.7903}
    W.~D.~Hillis and G.~L.~Steele
    \newblock Data Parallel Algorithms
    \newblock {\em Communications of the ACM}, 29(12):1170--1183,
    1986.
  \end{thebibliography}
\end{frame}


\end{document}

\usepackage{amssymb}
\usepackage[inference, shorthand]{semantic} % Inference rules, shortcuts

% ???
\usepackage[english]{babel}

% Make math look a little better
\usefonttheme[onlymath]{serif}
\usepackage{mathpazo}
\usepackage{eulervm}

% Use Raleway for most text
\usepackage{fontspec}
\defaultfontfeatures{Mapping=tex-text}
\setsansfont{Raleway}

................................................................................

\section{Background}


\begin{frame}\frametitle{Formal proofs}

Formal proofs --- an important component of computer science education.
\vfill
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^\mathit{R}$ is itself regular.
\end{itemize}

\end{frame}


\begin{frame}\frametitle{Paper proofs}

Paper proofs are common, but problematic for education:
\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}

................................................................................
\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}

\subsection{Proof assistants}

\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.
................................................................................
\end{itemize}

(End of aside.)

\end{frame}


\section{Proof assistants in education}

\begin{frame}\frametitle{Proof assistants in education}

We are interested in the application of proof assistants to CSCI education. 
\vfill
Why?
\begin{itemize}
\item Fixed notion of what a valid proof is (and isn't). 
\item Instant results: yes, this proof is correct; no, it isn't.
\item Interactive.
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Problems with existing systems}

But when it comes to undergrad education, there are some problems with 
existing systems:
\begin{itemize}
\item Complexity: powerful logics create complexity in even simple proofs.
\item Not user-friendly: Emacs + ProofGeneral are hardly intuitive.
\item Unfamiliar: Syntax often is often wildly different from any kind of 
  paper proof
\end{itemize}

\end{frame}

\begin{frame}\frametitle{What we don't want}

\begin{center}
\includegraphics[width=3.5in]{ebella.png}
\end{center}

\end{frame}

\begin{frame}\frametitle{What we do want}

\begin{center}
\includegraphics[width=3.5in]{proof-complete.png}
\end{center}

\end{frame}


\begin{frame}\frametitle{Demo}
\vfill
\centering
A quick demo of a proof in Arend
\vfill
\end{frame}

\section{Arend -- System description}

\begin{frame}\frametitle{What is Arend?}

Arend is a web-based proof assistant designed for use in undergraduate 
CSci education.
\vfill
\begin{itemize}
\item Based on a simple, familiar first order logic ($\forall$, $\exists$,
  $\land$, $\lor$, and $\to$).
\item \alert{Specifications} (systems to be reasoned about) are constructed
  by instructors, as are proof statements ($\forall X: \exists Y: \ldots$)
\item Students construct proofs by direct interaction: ``point-and-click''.
\item Invalid proofs cannot be constructed, and incomplete proofs are marked
  as such
\end{itemize}

\end{frame}

\subsection{Specification}

\begin{frame}[fragile]\frametitle{Specification logic}

Arend's specification logic is used to describe the systems to be reasoned
about. E.g., a specification for $\mathbb{N}, +$:

\begin{verbatim}
"Nat-z":   nat(z).
"Nat-s":   nat(succ(N)) :- nat(N).

"Add-z":   add(z,N,N).
"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
\end{verbatim}

\end{frame}

\begin{frame}\frametitle{Specification logic, cont.}

\begin{itemize}
\item A specification consists of a series of \alert{definitions}.
\item A definition consists of one or more \alert{clauses}.
\item Each clause has a name, a \alert{head}, and an (optional) \alert{body}.
\item The body of each clause must be a pure conjuction of atomic goals
  (calls to definitions)
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Almost Prolog...}

It looks like Prolog, but not quite:
\vfill
\begin{itemize}
\item No disjunction, except that implicit in multiple clauses.
\item No negation (``as failure'', or otherwise).
\item No proof search control structures: \texttt{!}, \texttt{->}, etc.
\end{itemize}
\vfill
Proof search (by resolution) is largely the same. (I.e., ordering of clauses
is significant for execution, but \emph{not} for proofs.)

\end{frame}

\begin{frame}[fragile]\frametitle{Specifications as rules}

Clauses in the specification logic correspond almost exactly to inference
rules:
\begin{verbatim}
"Add-z":   add(z,N,N).
"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
\end{verbatim}
becomes
\[
\inference[Add-z]
  {}
  {\mathsf{add}(z,N,N)}
\quad
\inference[Add-s]
  {\mathsf{add}(X,Y,Z)}
  {\mathsf{add}(\mathit{succ}(X),Y,\mathit{succ}(Z))}
\]

\end{frame}

\subsection{Reasoning logic}

\begin{frame}\frametitle{Reasoning logic}

Proofs are \alert{about} things in the specification logic, but proofs 
themselves are in the \alert{reasoning logic}.

The reasoning logic has everything the specification logic has, plus
\begin{itemize}
\item Implication: $P \to Q$. (Note that $P$ cannot contain further 
  implications!)
\item Explicit quantification: $\forall X: \ldots$ and $\exists Y: \ldots$
\item Free use of $\land$ and $\lor$
\end{itemize}

\end{frame}

\begin{frame}[fragile]\frametitle{Embedding}

Thus, the specification logic can be \alert{embedded} in the reasoning logic:
\begin{verbatim}
"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
\end{verbatim}
becomes
\[
\forall X,Y,Z: \mathsf{add}(X,Y,Z) \to 
  \mathsf{add}(\mathit{succ}(X),Y,\mathit{succ}(Z))
\]

\end{frame}

\begin{frame}\frametitle{Reasoning about specifications}

This allows us to use the specification logic to reason \alert{about}
specifications. E.g.
\vfill

\begin{beamerboxesrounded}[upper=block body,lower=block body,shadow=true]{Prove:}
\[
\forall X,Y: \mathsf{nat}(X) \land \mathsf{nat}(Y) \to 
  \exists Z: \mathsf{add}(X,Y,Z)
\]
\end{beamerboxesrounded}
\vfill
This proof will be \alert{about} nat and add.

\end{frame}

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


\section{Implementation}

\begin{frame}\frametitle{Implementation statistics}

Arend's implementation consists of:
\begin{itemize}
\item 1,401 lines of Prolog
\item 6,198 lines of Javascript (of which 442 lines are test
    code)
\item 493 lines of PEG grammar specification
\item 501 lines of HTML
\item 129 lines of CSS
\item 41 source code files in total
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Development details}

Arend's development:
\begin{itemize}
\item Tracked using the Fossil version control system 
  (\alert{\small http://fossil-scm.org})
\item 294 commits
\item Spans eight months of development
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Development tools}

Some libraries and tools used:
\begin{itemize}
\item Node.JS -- Offline Javascript runtime
\item SWI-Prolog -- Prolog environment
\item Lodash -- Javascript utility library
\item jQuery -- Javascript+HTML utility library
\item qUnit -- Javascript test framework
\item Pengines -- Prolog HTTP server framework
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Web client overview}

Arend's user interface is a fairly straightforward web client, with a few
twists:
\begin{itemize}
\item Full \texttt{Term} datatype (incl. atoms, logic variables, and compounds).
  This allows terms to be communicated to/from the backend without any 
  special-purpose translation.
\item Unification of terms is also present in the client codebase, currently
  unused. Eventually will form part of a term pattern-matching library.
\item Pengines allows (nearly) transparent JS/Prolog interop., almost as if
  Prolog was running in the browser.
\end{itemize}

\end{frame}

\subsection{Backend implementation}

\begin{frame}\frametitle{Major backend modules}

Arend's backend (exposed via HTTP) consists of three main modules:
\begin{itemize}
\item \texttt{subst} -- Unification and substitution
\item \texttt{program} -- Goal expansion and execution for specifications
\item \texttt{checker} -- Elaboration and checking of proofs (reasoning logic)
\end{itemize}
\end{frame}

\begin{frame}[shrink=20]\frametitle{Substitution and unification}

{\Large Because proofs may have different substitutions in different parts of the
tree, we cannot use Prolog's (global) unification and substitution. We 
reimplement logic variables, unification, and substitution.}
\vfill

\[
\inference[Case on $\mathsf{nat}$]
  {\inference[$X \mapsto z$]
    {\vdots}
    {\vdash \mathsf{add}(z,z,z)} &
   \inference[$X \mapsto s(N)$]
    {\vdots}
    {\mathsf{nat}(N) \vdash \mathsf{add}(s(N),z,s(N))}}
  {\mathsf{nat}(X) \vdash \mathsf{add}(X,z,X)}
\]


\end{frame}

\begin{frame}\frametitle{\texttt{subst} module}

The \texttt{subst} module implements:
\begin{itemize}
\item Custom variable type (encoded as special atoms)
\item Robinson unification algorithm over term containing these variables
\item Application of substitutions to terms
\end{itemize}

\end{frame}

\begin{frame}\frametitle{\texttt{program} module}

Module \texttt{program} is responsible for handling specifications: 
\begin{itemize}
\item Expanding calls to atomic goals (e.g., \texttt{add(z,s(z),X)}) requires
  renaming variables in the body, so they don't conflict
  with variables in scope.
\item Execution of specification queries follows the resolution proof
  search procedure. Note that Arend lacks ``negation as failure''. 
\item Execution produces proof objects compatible with those used by the
  full proof checker.
\item Execution of queries is exposed via the \texttt{repl} Pengine application.
\end{itemize}

\end{frame}

\begin{frame}\frametitle{\texttt{checker} module}

The most complex module in the backend, \texttt{checker} handles elaboration
and checking of proofs in the full reasoning logic.

\begin{itemize}
\item Proof \alert{completeness} -- Does a proof contain any holes?
  (Simple recursive predicate)
\item Proof \alert{elaboration} -- Expanding a hole into a 1-level subproof
\item Proof \alert{checking} -- Is a proof correct, according to a 
  specification and the rules of the reasoning logic?
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Proof elaboration}

Proof elaboration, in tandem with proof checking, is at the heart of 
incremental proof construction. Consider the proof state:
\[
\inference[]
  {?}
  {\vdash P \land Q}
\]
\vfill
If we elaborate $P \land Q$, what should replace ?.

\end{frame}

\begin{frame}\frametitle{Proof elaboration, cont.}

\[
\inference[]
  {\inference[]{?}{\vdash P} &
   \inference[]{?}{\vdash Q}}
  {\vdash P \land Q}
\]
\vfill
Elaboration expands a ?, in combination with either the consequent or an
antecedant, so that the result is a valid proof tree, one level deeper.

\end{frame}

\begin{frame}\frametitle{Proof checking}

Checking a proof object proceeds by checking it against the \alert{rules}
of the specification logic.
\vfill
\[
\inference[$\wedge_R$]
    {\Gamma |- P & \Gamma |- Q}
    {\Gamma |- P \wedge Q}
\quad
\inference[$\wedge_L$]
    {\Gamma, P, Q |- G}
    {\Gamma, P \wedge Q |- G}
\]
(E.g.: Rules for $\land$)

\end{frame}

\begin{frame}\frametitle{Proof checking, cont.}

Each node of the proof tree includes:
\begin{itemize}
\item Node type (e.g., \texttt{product}, \texttt{induction}, etc.)
\item Subproof(s) (child nodes)
\item Consequent (proposition to the right of $\vdash$)
\item Antecedents (propositions to the left of $\vdash$)
\item Current substitution
\item Variables in scope
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Proof checking, cont.}

Substitutions and variable bindings flow through the tree nontrially:
\vfill
\begin{itemize}
\item Substitutions flow from leaves to root, but also left-to-right in 
  conjunctions.
\item Variable scopings flow from root to leaves, but also left-to-right in
  conjunctions.
\end{itemize}
\vfill
Formalization of the complete proof checking procedure, including substitutions
and variable scopings, is ongoing.

\end{frame}

\begin{frame}\frametitle{Proof construction procedure}

\begin{enumerate}
\item User selects an element (antecedent or consequent) in the current proof
  state. Path to the element along with the proof tree is passed to the server.
\item Path to the element along with the proof tree is passed to the server.
\item Server calls \texttt{checker:elaborate} to elaborate the desired element.
\item Elaborated proof is returned to client.
\item New proof is checked for completeness. Complete? then \textsc{Stop}, else
  \textsc{GoTo} 1.
\end{enumerate}

\end{frame}

\section{Future work}

\begin{frame}\frametitle{The future of Arend}

Arend is far from complete; enhancements can be divided into three areas:

\begin{itemize}
\item Necessary features 
\item Enhancements
\item Formalization
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Necessary features}

Arend is missing many features that would be necessary in a large-scale
deployment:
\begin{itemize}
\item Centralized storage of specifications, assignments
\item Interop with grading backend, for storage of (in)complete assignments
\item Richer user interface: lemma construction, instantiation of $\exists$
  variables, etc. are all unspecified
\item Easy-to-deploy packaging of the entire system
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Enhancements}

Although not strictly necessary, there are still many enhancements that would 
make Arend a better system, either more powerful, easier to use, or both.
\begin{itemize}
\item Enhanced proofs: tactics, instructor-controlled proof automation.
\item Support for student-authored specifications
\item Alternate proof interfaces: traditional paragraph, mixed, etc.
\item Functional language for reasoning about programs, equational reasoning
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Formalization}

Although we believe Arend's systems to be fully adequate, being based on
existing well-studied systems, a full formalization of our systems and their
integration would be a useful addition.
\begin{itemize}
\item Full operational semantics of the specification logic
\item Proof of soundness and non-deterministic completeness of the 
  specification logic (all things proven are true, and nothing false can be
  proven)
\item Full semantics for reasoning logic, incl. substitutions and bindings
\item Proof of \alert{adequecy} of the reasoning logic with regard to the
  specification logic.
\end{itemize}

\end{frame}

\begin{frame}\frametitle{Conclusions}

We believe that Arend's design will make it a valuable addition to the
undergraduate computer science curriculum. We are currently working to get
Arend into a suitable state for use in our own courses, and hope to have 
feedback from real student usage in the future.

\end{frame}


%%% --------------------------------------------------------------------------
%%% Bibliography slide
%%% --------------------------------------------------------------------------

................................................................................
\section<presentation>*{\appendixname}
\subsection<presentation>*{For Further Reading}

\begin{frame}{For Further Reading}
    
  \begin{thebibliography}{10}
    
  \beamertemplatearticlebibitems


  \bibitem{clifton2015arend}
    A.~V.~Clifton
    \newblock Arend --- Proof-assistant Assisted Pedagogy

    \newblock CSU Fresno, 2015.
    

  \beamertemplatearticlebibitems


  \bibitem{geuvers2009proof}
    H.~Geuvers
    \newblock Proof assistants: History, ideas and future
    \newblock {\em Sadhana}, 31(1):3--25,
    Springer, 2009.



  \end{thebibliography}
\end{frame}


\end{document}