Reading: In this part of the course I followed Chapters 1-8 of Gilmore's notes fairly closely although I omitted a few topics, stressed some topics more or less than he did, modified the order of presentation in several places and used variants of one or two of his examples. Essentially the same material is covered in almost any book or tutorial on SML including Paulson's book and Harper's notes, and reading any one of these would usefully complement the presentation in the lectures.
Revising: Compare the sample solution to Practical 1 with your own solution. Do some exercises from Paulson's book.
What you are expected to know: The stress here is not on the details of the syntax of SML but rather on the underlying concepts and the way that one expresses algorithms and represents data in a functional language. So examination questions might be along lines like "Write a program to do X" rather than "List the keywords of SML in alphabetical order". You will not be asked to write very long programs and when marking I will ignore minor mistakes with the syntax of SML. I expect you to be able to make reasonable use of the features of the SML core language. I do not expect intimate knowledge of SML input/output or of the SML library.
Reading: In this part of the course I did not follow any of the references but the material I covered can be found in Paulson's book or Harper's notes. The coverage of modules in chapter 9 of Gilmore's notes is not extensive enough for the purposes of this couse.
Revising: Compare the sample solution to Practical 2 with your own solution. Do some exercises from Paulson's book.
What you are expected to know: Again, the stress is on concepts rather than syntax. I expect you to be able to make reasonable use of the SML module facilities to organize SML programs, and to understand the issues involved in modular design. Because of time constraints, examination questions involving modules are by necessity sketchy about the details of the code in the modules. You would not normally be asked to design a module structure and write code from scratch to go in the modules.
Reading: In this part of the course I followed the sequence of examples in my paper "Formal specification of ML programs" and the presentation of stepwise development and parts of the presentation of EML in my paper "Formal program development in Extended ML for the working programmer". As in those papers, attention is restricted to total functions that return non-exceptional values in this part of the course. Some other papers on EML do not make this restriction. Kahrs's notes are worth reading but for my taste they put too much emphasis on side issues.
Revising: Compare the sample solution to Practical 3 (forthcoming) with your own solution. Find old APS exam papers (they should be in the JCM library) and do the questions involving specification and proof. Read VanInwegen's notes on how to write proofs.
What you are expected to know: I expect you to be able to use EML to specify SML programs, to verify the correctness of programs with respect to such specifications, and to understand the issues involved in program specification and verification. The precise syntax of axioms in EML is not important, but axioms should be understandable as formal assertions in first-order logic. In specifying programs, concentrate on giving properties that the program must satisfy and forget about how the specified behaviour will be implemented unless you are asked for an implementation. In proofs, concentrate first on stating clearly what it is you are trying to prove. Proving properties of recursive programs will usually require the use of structural induction with respect to the argument type. In induction proofs, the most important thing is to be clear in the "step" case about what the induction hypothesis is and what it is that you are trying to prove using this hypothesis.