Halfway through adding material on experience teaching the course

papers/scp/PLFA.tex

@@ -803,6 +803,116 @@ notably by \citet{Chapman-2009} and \citet{Allais-et-al-2017}.
 Philip is grateful to David Darais for bringing it to his attention.
 
 
+\section{Experience}
+
+Philip now has five years of experience teaching from SF and one year
+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.
+
+\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.
+
+\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.
+    
+\end{itemize}
+In addition, David Darais at University of Vermont and John Leo at
+Google Seattle have taught from PLFA.
+
+Exercises in PLFA are classified in three ways.
+\begin{itemize}
+\item
+  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.
+
+\item   
+  Exercises without a label are included for those who want extra
+  practice.  To Philip's surprise, students at PUC-Rio completed
+  quite a few of these.
+\end{itemize}
+Students are expected to complete coursework for all of the
+required questions in the text, optionally doing any stretch or
+unlabelled exercises. Coursework also includes a ``mock mock''
+exam, as described below.
+
+The mark for the course is based on coursework and a final-exam,
+weighted 1/4 for coursework and 3/4 for the final exam.  The weighting
+for coursework is designed to be high enough to encourage students to
+do it (they all do), but not so high as to encourage cheating.
+Students are encouraged to help each other with coursework.
+
+The final-exam is two hours online. Students have access to the Agda
+proof assistant to check their work.  At Edinburgh, students use
+computers with a special exam operating system that disables access
+to the internet.  Students are given access to the text of PLFA,
+the Agda standard libraries, and the Agda language reference manual,
+but no other materials.
+
+Students must answer question 1 on the exam, and one of questions 2 or
+3.  Question 1 gives predicates over a data structure, such lists or
+trees, to be formalised in Agda, and a theorem relating the
+predicates, to be formalised and proved in Agda.  Question 2 gives the
+students the intrinsic formulation of lambda calculus from chapter
+DeBruijn, which they must extend with a described language feature.
+Question 3 give the students the the bidirectional type inferencer
+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.
+
+
+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 
+
 \section{Conclusion}
 
 We look forward to experience teaching from the new text,