John Harrison
Computer Science Tripos, Part II (General) and Diploma in Computer Science
Twelve lectures, beginning on Fri 16th Jan 1997, ending on Tue 11th Feb 1997
Tuesday, Thursday & Friday at 12:00 in the
Hopkinson Lecture Room
Lecture Notes
Entire notes (160 pages):
DVI,
Postscript
- Title, preface, table of contents:
DVI,
Postscript
- Chapter 1 - Introduction:
DVI,
Postscript
- Chapter 2 - Lambda calculus:
DVI,
Postscript
- Chapter 3 - Lambda calculus as a programming language:
DVI,
Postscript
- Chapter 4 - Types:
DVI,
Postscript
- Chapter 5 - A taste of ML:
DVI,
Postscript
- Chapter 6 - Further ML:
DVI,
Postscript
- Chapter 7 - Proving programs correct:
DVI,
Postscript
- Chapter 8 - Effective ML:
DVI,
Postscript
- Chapter 9 - Examples:
DVI,
Postscript
- References:
DVI,
Postscript
Copies of slides
- Introduction and Overview:
Colour Postscript
- Lambda calculus as a formal system:
Colour Postscript
- Lambda calculus as a programming language:
Colour Postscript
- Types:
Colour Postscript
- ML:
Colour Postscript
- Details of ML:
Colour Postscript
- Proving programs correct:
Colour Postscript
- Effective ML:
Colour Postscript
- ML examples I: Symbolic differentiation:
Colour Postscript
- ML examples II: Recursive descent parsing:
Colour Postscript
- ML examples III: Exact real arithmetic:
Colour Postscript
- ML examples IV: Prolog and theorem proving:
Colour Postscript
Additional material is available from those who have taught
the course in previous years: Mike Gordon
and Andy
Gordon. The theoretical part of the course is also covered by lecture
notes from Larry
Paulson.
Syllabus
This describes roughly how the course was taught over 12 lectures, each of
slightly less than an hour. Only what was actually taught will be examinable.
- Introduction and Overview Functional and imperative
programming: contrast, pros and cons. General structure of the course: how
lambda calculus turns out to be a general programming language. Lambda
notation: how it clarifies variable binding and provides a general analysis of
mathematical notation. Currying. Russell's paradox.
- Lambda calculus as a formal system Free and bound
variables. Substitution. Conversion rules. Lambda equality. Extensionality.
Reduction and reduction strategies. The Church-Rosser theorem: statement and
consequences. Combinators.
- Lambda calculus as a programming language Computability
background; Turing completeness (no proof). Representing data and basic
operations: truth values, pairs and tuples, natural numbers. The predecessor
operation. Writing recursive functions: fixed point combinators. Let
expressions. Lambda calculus as a declarative language.
- Types Why types? Answers from programming and logic.
Simply typed lambda calculus. Church and Curry typing. Let polymorphism.
Most general types and Milner's algorithm. Strong normalization (no proof), and
its negative consequences for Turing completeness. Adding a recursion operator.
- ML ML as typed lambda calculus with eager evaluation.
Details of evaluation strategy. The conditional. The ML family. Practicalities
of interacting with ML. Writing functions. Bindings and declarations. Recursive
and polymorphic functions. Comparison of functions.
- Details of ML More about interaction with ML. Loading
from files. Comments. Basic data types: unit, booleans, numbers and strings.
Built-in operations. Concrete syntax and infixes. More examples. Recursive
types and pattern matching. Examples: lists and recursive functions on lists.
- Proving programs correct The correctness problem. Testing
and verification. The limits of verification. Functional programs as
mathematical objects. Examples of program proofs: exponential, GCD, append and
reverse.
- Effective ML Using standard combinators. List iteration
and other useful combinators; examples. Tail recursion and accumulators; why
tail recursion is more efficient. Forcing evaluation. Minimizing consing. More
efficient reversal. Use of `as'. Imperative features: exceptions, references,
arrays and sequencing. Imperative features and types; the value restriction.
- ML examples I: symbolic differentiation Symbolic
computation. Data representation. Operator precedence. Association lists.
Prettyprinting expressions. Installing the printer. Differentiation.
Simplification. The problem of the `right' simplification.
- ML examples II: recursive descent parsing Grammars and
the parsing problem. Fixing ambiguity. Recursive descent. Parsers in ML. Parser
combinators; examples. Lexical analysis using the same techniques. A parser for
terms. Automating precedence parsing. Avoiding backtracking. Comparison with
other techniques.
- ML examples III: exact real arithmetic Real numbers and
finite representations. Real numbers as programs or functions. Our
representation of reals. Arbitrary precision integers. Injecting integers into
the reals. Negation and absolute value. Addition; the importance of rounding
division. Multiplication and division by integers. General multiplication.
Inverse and division. Ordering and equality. Testing. Avoiding reevaluation
through memo functions.
- ML examples IV: Prolog and theorem proving Prolog terms.
Case-sensitive lexing. Parsing and printing, including list syntax.
Unification. Backtracking search. Prolog examples. Prolog-style theorem
proving. Manipulating formulas; negation normal form. Basic prover; the use of
continuations. Examples: Pelletier problems and whodunit.
Papers and documentation online
Here are some useful books, papers and tutorials online. They might save a trip
to the library.
Online ML resources
This is a collection of other Web links that are relevant to the material we
cover in the second part of the course.