finished segment on exams

papers/scp/PLFA.tex

@@ -810,22 +810,24 @@ teaching from PLFA.  He taught three courses from PLFA.
 \begin{itemize}
 \item
   University of Edinburgh, September--December 2018 (with teaching
-  assistance from Wen and Chad Nester); twenty two-hour slots, one
+  assistance from Wen and Chad Nester); twenty two-hour slots,
-  hour of lecture followed by one hour of lab. Ten students completed
+  comprising one hour of lecture followed by one hour of lab. Ten
-  the course, which covered Parts~I and~II of PLFA.
+  students completed the course, fourth-year undergraduates and
+  masters.  The course covered Parts~I and~II of PLFA.
 
 \item
   Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
   March--July 2019, hosted by Roberto Ieuramalischy; ten three-hour
-  slots, two hours of lecture followed by one hour of lab.  Ten
+  slots, comprising two hours of lecture followed by one hour of lab.
-  students completed the course, which covered Parts~I and~II of PLFA,
+  Ten students completed the course, mostly doctoral students.  The
-  save students read chapter Lists on their own, and chapter
+  course covered Parts~I and~II of PLFA, save students read chapter
-  Bisimilarity was skipped.
+  Lists on their own, and chapter Bisimilarity was skipped.
 
-\item University of Padova, June 2018, hosted by Maria Emilia Maietti;
+\item
-  two three-hour slots, two hours of lecture followed by one hour of
+  University of Padova, June 2018, hosted by Maria Emilia Maietti; two
-  lab.  About thirty students sat the course. Covered chapters
+  three-hour slots, comprising two hours of lecture followed by one
-  Naturals, Induction, and Relations.
+  hour of lab.  Thirty undergraduate students sat the course, which
+  covered chapters Naturals, Induction, and Relations.
     
 \end{itemize}
 In addition, David Darais at University of Vermont and John Leo at
@@ -837,11 +839,10 @@ Exercises in PLFA are classified in three ways.
   Exercises labelled “(recommended)” are the ones students are
   required to do in the classes taught at Edinburgh and PUC-Rio.
 
-
 \item
   Exercises labelled “(stretch)” are there to provide an extra
   challenge. Few students do all of these, but most attempt at least a
-  few.  Ten students completed the course.
+  few. 
 
 \item   
   Exercises without a label are included for those who want extra
@@ -877,41 +878,52 @@ from chapter Inference, which they must extend with a described
 language feature.
 
 Because the course is taught using a proof assistant, it is important
-that the students have access to a proof assistant during the
+that students have access to a proof assistant during the exam.
-exam. The whole point of a proof assistant is to avoid
+Students are told in advance that they are expected to get perfect on
-errors. Students are told in advance that they are expected to get
+the exam, and that they will have to study hard to achieve this level.
-perfect on the exam, and that they will have to study hard to achieve
+Given that the goal of formal methods is to avoid error, we believe a
-this level.  Given that the goal of formal methods is to avoid error,
+pedagogical purpose is served by telling the students that they are
-we think a pedagogical purpose is served by telling the students that
+expected to achieve perfection and making it possible for them to do
-they are expected to achieve perfection and making it possible for
+so.  Students are given two opportunities to practice in the run up to
-them to do so.
+the exam, a `mock' exam given in class under exam conditions (two
+hours online), and before that a `mock mock' exam as coursework (in
+their own time, encouraged to ask questions, tasked to do all three
+questions rather than two of three).
 
+Table~\ref{tab:exams} shows performance on the mock exam and the final
+exam for the courses run at Edinburgh and PUC-Rio.  While scores vary
+widely on the mock, all students achieve perfection on the
+exam.  (The one exception was a PUC-Rio student who did not attend
+classes or sit the mock.)  Similar results were achieved at Edinburgh
+over the previous five years, using SF as the course textbook and Coq
+as the proof assistant.  We consider these results a tribute to the
+students' ability to study and learn.
 
-they are expected to answer
+\begin{table}
-one question about formalising predicates on a data structure such
+\begin{center}
-as lists or tree
+  \begin{tabular}{|cc|cc|}
-
+    \hline
-
+    \multicolumn{2}{|c|}{Edinburgh} &
-
+    \multicolumn{2}{c|}{PUC-Rio} \\
-
+    \hline
-The coursework is assigned 1/4 of the
+    Mock & Exam & Mock & Exam \\
-total mark of the course: enough to encourage the students to do
+    \hline
-it, but not enough to make it worth cheating. The remaining 3/4 of
+     15  &  50  &  --  &  40  \\
-the tot
+     29  &  50  &  ~6  &  50  \\
-
+     33  &  50  &  20  &  50  \\
-Most of the marks are base 
+     35  &  50  &  28  &  50  \\
-
+     36  &  50  &  41  &  50  \\
-
+     48  &  50  &  49  &  50  \\
-There is also a ``mock mock'' exam
+     49  &  50  &  50  &  50  \\
-assigned as cou
+     50  &  50  &  50  &  50  \\
-
+     50  &  50  &  50  &  50  \\
-The coursework was broken into four or five clusters, one due every
+     50  &  50  &  50  &  50  \\
-few weeks. There is also a coursework consisting of a ``mock mock''
+    \hline
-exam, see below.  
+  \end{tabular}
-
+\end{center}
-
+\caption{Exam marks}
-recommended
+\label{tab:exam}
-At Edinburgh and PUC-Rio, students completed coursework based on 
+\end{table}
 
 \section{Conclusion}