ML for the Working Programmer

Part 1 Introduction: functional programming; standard ML. Part 2 Names, functions and types: value declarations; numbers, character strings, truth values; pairs, tuples and records; the evaluation of expressions; writing recursive functions; local declarations; polymorphic type checking. Part 3 Lists: introduction to lists; some fundamental list functions; applications of lists; the equality test in polymorphic functions; sorting - a case study. Part 4 Trees and concrete data: the datatype declaration; exceptions; trees; functional arrays and priority queues; A lists; search strategies and lazy lists. Part 6 Reasoning about functional programs: some principles of mathematical proof; structural induction; a general induction principle; specification and verification. Part 7 Modules: queues, an abstract type; structures; signatures of structures; functors over structures; a review of the modules system. Part 8 Imperative programming in ML: reference types; references in data structures; input and output in Standard ML. Part 9 Writing interpreters for the pye calculus: a functional parser; the pye calculus; representing pye terms in ML; the pye calculus as a programming language. Part 10 A tactical theorem prover: a sequent calculus for first-order logic; processing terms and formulae in ML; tactics and the proof state; searching for proofs.