**Reading:**
In this part of the course I followed chapters 2-14 of
Harper's book
fairly closely although I omitted a few topics, stressed some
topics more or less than he did and used variants of one or two of his
examples.
I covered the material in his chapter 15 in quite a different way; see
Lecture Note 1.
A topic that is missing from Harper's book (equality types)
is covered on the last half-page of that note.
Essentially the same material is covered in almost any book
or tutorial on ML including
Paulson's book
(chapters 1-5 and 8, minus the stuff about structures and signatures)
and
Gilmore's tutorial
(all except the last chapter),
and reading any one of these would usefully complement the
presentation in the lectures. Another source is chapters 1, 2 and 4 of
the precursor to Harper's book,
This covers a dialect of ML that is now obsolete, but
the differences
are very minor. It is nice and short and so still worth reading as a
summary of the main important ideas in ML.
Another short summary, written by a previous FPS student, is
here.
(Disclaimer: I have not read this in detail!
If it contains errors or misleading information then that is your problem.)

**Revising:**
Read your tutor's comments on your solution to
Practical 1.
Use these comments to improve your solution.
After doing this, compare
the sample solution to Practical 1
with your solution.
Do some exercises from
Paulson's book.

**What you are expected to know:** The stress is on the underlying
concepts and the way that one expresses algorithms and represents data
in a functional language. You will be expected to produce working
programs, but you will have the ML compiler and typechecker to help you.
I expect you to be able to make reasonable use of the features of the
ML core language.
The Moscow ML library and its documentation will be available.

**Reading:**
In this part of the course I followed chapters 18-23 of
Harper's book.
This material is not covered well in some books and tutorials on ML;
in particular, the coverage of modules in the last chapter of
Gilmore's notes
is not extensive enough for the purposes of this course.
Alternative presentations of the material are in
Paulson's book
(the stuff about structures and signatures in chapters 2-5, plus
chapter 7)
and
Tofte's lecture notes.
Another source is chapter 3 of
the precursor to Harper's book.
The chapters of Harper's book that cover modules contain more errors
than the earlier chapters and the explanation is lacking in places.
Since many people find this material a little difficult, I recommend
that you consult one of these other sources as well.

**Revising:**
Read your tutor's comments on your solution to
Practical 2.
Use these comments to improve your solution.
After doing this, compare
the sample solution to Practical 2
with your solution.
Do some exercises from
Paulson's book
and/or the exercise in part 2 of
Tofte's lecture notes.

**What you are expected to know:**
Again, the stress is on concepts. I expect you to
be able to make reasonable use of the ML module facilities to
organize ML programs, and to understand the issues involved in
modular design.
Examination questions involving modules generally do not involving
writing a lot of code;
you would not normally be asked to design a module structure
*and* write code from scratch to go in the modules.
You will have the ML compiler and typechecker to help you sort out
sharing problems etc.

**Reading:**
Most of what you need to know about the material in this part of the
course is in the following lecture notes:

- Specifying functions in Extended ML
- Proving that a function meets its specification (See chapter 26 of Harper's book and chapter 6 of Paulson's book for alternative presentations of part of this material.)
- Specifying structures in Extended ML
- Proving that a structure meets its specification

**Revising:**
Read your tutor's comments on your solution to
Practical 3.
Use these comments to improve your solution.
After doing all this,
compare the sample solution to Practical 3
with your solution.
Read
VanInwegen's notes on how to write proofs.
Practice doing proofs by induction, using the examples covered in
lectures.
Try specifying some basic functions and data structures like the ones in
the Moscow ML library.

**What you are expected to know:**
I expect you to be able to use EML to specify ML programs (involving
only total functions returning non-exceptional values)
and
to verify
the correctness of programs with respect to such specifications.
The precise syntax of
axioms in EML is not important, but axioms must 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.
The second most important thing is to make it clear where in the proof
you make use of this hypothesis.

Don Sannella. Please mail me if you have any comments on this page. Last modified: Sat Apr 30 12:58:11 BST 2011