Check-in [dab782646e]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Full presentation (still draft).
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:dab782646e831d96b86c29452f4fd405808e5532
User & Date: andy 2015-04-26 21:15:02
Context
2015-04-27
12:59
Just making sure the poster was up-to-date. check-in: 6466816782 user: andy tags: trunk
2015-04-26
21:15
Full presentation (still draft). check-in: dab782646e user: andy tags: trunk
16:27
Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk
Changes
Hide Diffs Unified Diffs Show Whitespace Changes Patch

Changes to presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

25
26
27
28
29
30
31


32
33
34
35
36
37
38
..
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
...
102
103
104
105
106
107
108

109
110
111
112
113
114
115
...
169
170
171
172
173
174
175

176

177









































178
179
180
181
182










































































































































































































































































































































































































































183
184
185
186
187
188
189
...
191
192
193
194
195
196
197
198
199
200

201
202
203
204
205
206
207
208
209



210
211
212
213
214
215
216
217
218
219
\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}







>
>







 







|





|







|







 







>







 







>

>

>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|




>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







|
<

>
|
|
<
|
|
<

<

>
>
>
|
|
<
<
<





25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
..
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
...
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
...
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
...
663
664
665
666
667
668
669
670

671
672
673
674

675
676

677

678
679
680
681
682
683



684
685
686
687
688
\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}