Applicative Programming and Specification

This module has been replaced by Functional Programming and Specification. Everything below is from 2000/2001 which is the last time this module was taught.

Time, place and scope

This module runs in term 2. The official syllabus is here. Lectures take place in JCMB 3317 on Tuesdays 12-1 and Fridays 3-4; there are no tutorials.

Here is a detailed summary of what I covered and what I expect students to have learned.

Lecture log and examples

The lecture log is a concise record of the lectures on the course.

These examples from the lectures are suitable for cutting and pasting into an SML or EML session.

Shortcuts: SML core language examples, SML module language examples, EML examples

Running SML'97

On Linux

Type mosml to the shell to start Moscow ML version 2.00. Then type use "file.sml"; to load an SML source file called file.sml.

Documentation: try typing help "topic"; in Moscow ML for information about topic. There are various manuals at the Moscow ML website, including the Moscow ML library manual (2-up postscript version).

If you have a home machine

Moscow ML version 2.00 is free and can be downloaded from here. (You can borrow a CD ROM with this on it from the Support Office in JCMB 2421.)

Running EML'90

On Linux

Type eml to the shell to run the Warsaw EML Kit parser/typechecker (v1.1). Then type use "file.eml" to load the contents of file.eml. Type control-D to quit.

If you have a home machine

The Warsaw EML Kit (v1.1) can be downloaded from these local copies: eml11-src.tar.gz (source) eml11-i386.tar.gz (i386 Linux binaries) eml11-sparc.tar.gz (Sun SPARC Solaris binaries), or directly from Warsaw.

Here are a couple of tips on getting the Extended ML system to accept your specifications.

Reading list

S. Gilmore. Programming in Standard ML'97: A tutorial introduction. Edinburgh report ECS-LFCS-97-364, 1997. This is essential reading for the first part of the course. It is available in the Computer Science reports room or in various printable formats. A slightly revised version of this is available as hypertext, or for printing. Here is a list of some relevant differences between the two versions.

R. Harper. Programming in Standard ML. Carnegie Mellon University, 1998. The part of this covering modules is essential reading for the second part of the course. The author states that it is work in progress but it seems stable enough for our use. It is available in hypertext and in pdf: for reading (local copy of 19/12/2000), for printing (local copy of 19/12/2000).

M. Tofte. Essentials of Standard ML modules. Notes for Summer School on Advanced Functional programming, held at the Oregon Graduate Institute, August, 1996. This is an alternative to the modules part of Harper's notes.

D. Sannella. Formal specification of ML programs. Jornadas Rank Xerox Sobre Inteligencia Artificial Razonamiento Automatizado, 79-98, 1987. Edinburgh report ECS-LFCS-86-15. This is essential reading for the third part of the course. It is available in the Computer Science reports room, or in postscript.

D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park, 1990. Springer Workshops in Computing, 99-130, 1991. Edinburgh report ECS-LFCS-89-102. Parts of this are essential reading for the third part of the course. It is available in the Computer Science reports room, or in postscript.

L. Paulson. ML for the Working Programmer, second edition. Cambridge University Press, 1996. Currently £21.95 in paperback. If you want to buy a book, this is the one to get. Its coverage of the material in the first two parts of the course is very good. If you buy it then you won't need to refer to Gilmore's or Harper's notes. The examples in the book are here; answers to selected exercises are here; errata are here.

J. Ullman. Elements of ML Programming, second edition. Prentice-Hall, 1997. Currently £34.99 in paperback. This is a possible alternative to Paulson's book for the first two parts of the course.

S. Kahrs. Lecture notes on formal program development. Report ECS-LFCS-97-372, 1997. This is for people who want to know more about the third part of the course than what is covered in the lectures. It is available in the Computer Science reports room, or in various printable formats.

Standard ML resources

¤ The Comp.Lang.ML newsgroup and its FAQ ¤ Moscow ML ¤ Moscow ML CGI interface ¤ Standard ML of New Jersey ¤ A Gentle Introduction to ML ¤ Chris Reade's book and ML code ¤ Mads Tofte's papers ¤ Mads' "Tips for Computer Scientists On Standard ML" ¤ Andrew Appel's papers ¤

Some Standard ML papers for background reading

¤ How ML Evolved, Robin Milner ¤ A Standard ML Compiler, Andrew Appel and Dave MacQueen ¤ Standard ML of New Jersey, Andrew Appel and Dave MacQueen ¤ A run-time system, Andrew Appel ¤ A Critique of Standard ML, Andrew Appel ¤ A Tutorial on Co-induction and Functional Programming, Andrew Gordon ¤ Simple Imperative Polymorphism, Andrew Wright ¤ Principal type-schemes for functional programs, Luis Damas and Robin Milner ¤ Type Systems, Luca Cardelli ¤ A semantics for ML concurrency primitives, Dave Berry, Robin Milner and David Turner ¤

Related languages

CAML: CAML light and Objective CAML (CAML light plus objects and classes) ¤ Haskell, a lazy functional language ¤ DML, an extension of ML with restricted dependent types ¤ Cayenne, a Haskell-like language with dependent types