- p.2: superdelopments -> superdevelopments
- p.3+35: Curch -> Church
- p.17: footnote 4 is repeated 3 lines below
- p.18: Exercise 3: 0 should be underlined
- p.24: Lemma 8: beta-reduction instead of abstract ->
- p.27: Exercise 7: sr=s -> sr=r
- p.33: wrong quote signs in the parts of the proof of the theorem
- p.36: Exercise 15 (a) shall have parts (i) and (ii) and not twice (i).
- p.38: Lemma 23, second line of proof: t:tau -> t:rho
- p.39: measure h is defined as a natural number or 0 and in part II, p.15, defined differently as a natural number (which is assumed to include 0).
- p.40: last case has t and t vector instead of s and s vector
- p.41 (the second most serious typo): The first application of Lemma 21(b) gives rho such that y vector s has type tau in the context Delta, y:rho (instead of Delta only).
- p.43: The definition of type substitution shall in the case for all require beta not in alpha or free in sigma (alpha and beta swapped), and this is achieved by renaming the bound variable beta!
- p.43:[Bar 93] is not part of the name "system F in Curry-style" but only a reference where this naming can be found
- p.43: with rho replaced by any type sigma -> with alpha replaced by any type sigma
- p.55: second diagram needs s -> sigma
- p.56: final paragraph needs an r' instead of r in the first case for t
- p.60 (the most serious typo): In the conclusion of Lemma 49 one has to use the transitive reflexive closure of the relation and not the relation alone.

Ralph Matthes Last modified: Thu Nov 2 16:23:19 CET 2000