From e2389f26f452a801ccf5841fb77d0e09146545fa Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 15 Jul 2019 08:43:24 +0100 Subject: [PATCH] finished segment on exams --- papers/scp/PLFA.tex | 104 ++++++++++++++++++++++++-------------------- 1 file changed, 58 insertions(+), 46 deletions(-) diff --git a/papers/scp/PLFA.tex b/papers/scp/PLFA.tex index 34c143df..7a57981e 100755 --- a/papers/scp/PLFA.tex +++ b/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 - hour of lecture followed by one hour of lab. Ten students completed - the course, which covered Parts~I and~II of PLFA. + assistance from Wen and Chad Nester); twenty two-hour slots, + comprising one hour of lecture followed by one hour of lab. Ten + 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 - students completed the course, which covered Parts~I and~II of PLFA, - save students read chapter Lists on their own, and chapter - Bisimilarity was skipped. + slots, comprising two hours of lecture followed by one hour of lab. + Ten students completed the course, mostly doctoral students. The + course covered Parts~I and~II of PLFA, save students read chapter + Lists on their own, and chapter Bisimilarity was skipped. -\item University of Padova, June 2018, hosted by Maria Emilia Maietti; - two three-hour slots, two hours of lecture followed by one hour of - lab. About thirty students sat the course. Covered chapters - Naturals, Induction, and Relations. +\item + University of Padova, June 2018, hosted by Maria Emilia Maietti; two + three-hour slots, comprising two hours of lecture followed by one + 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 -exam. The whole point of a proof assistant is to avoid -errors. Students are told in advance that they are expected to get -perfect on the exam, and that they will have to study hard to achieve -this level. Given that the goal of formal methods is to avoid error, -we think a pedagogical purpose is served by telling the students that -they are expected to achieve perfection and making it possible for -them to do so. +that students have access to a proof assistant during the exam. +Students are told in advance that they are expected to get perfect on +the exam, and that they will have to study hard to achieve this level. +Given that the goal of formal methods is to avoid error, we believe a +pedagogical purpose is served by telling the students that they are +expected to achieve perfection and making it possible for them to do +so. Students are given two opportunities to practice in the run up to +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 -one question about formalising predicates on a data structure such -as lists or tree - - - - -The coursework is assigned 1/4 of the -total mark of the course: enough to encourage the students to do -it, but not enough to make it worth cheating. The remaining 3/4 of -the tot - -Most of the marks are base - - -There is also a ``mock mock'' exam -assigned as cou - -The coursework was broken into four or five clusters, one due every -few weeks. There is also a coursework consisting of a ``mock mock'' -exam, see below. - - -recommended -At Edinburgh and PUC-Rio, students completed coursework based on +\begin{table} +\begin{center} + \begin{tabular}{|cc|cc|} + \hline + \multicolumn{2}{|c|}{Edinburgh} & + \multicolumn{2}{c|}{PUC-Rio} \\ + \hline + Mock & Exam & Mock & Exam \\ + \hline + 15 & 50 & -- & 40 \\ + 29 & 50 & ~6 & 50 \\ + 33 & 50 & 20 & 50 \\ + 35 & 50 & 28 & 50 \\ + 36 & 50 & 41 & 50 \\ + 48 & 50 & 49 & 50 \\ + 49 & 50 & 50 & 50 \\ + 50 & 50 & 50 & 50 \\ + 50 & 50 & 50 & 50 \\ + 50 & 50 & 50 & 50 \\ + \hline + \end{tabular} +\end{center} +\caption{Exam marks} +\label{tab:exam} +\end{table} \section{Conclusion}